mmtheorems91 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10774

Statement List for Metamath Proof Explorer - 9001-9100 - Page 91 of 108

Type	Label	Description
Statement
Theorem	normgt0tOLD 9001	The norm of non-zero vector is positive.
|- (A e. H~ -> (-. A = 0h <-> 0 < (normh` A)))
Theorem	normgt0t 9002	The norm of non-zero vector is positive.
|- (A e. H~ -> (A =/= 0h <-> 0 < (normh` A)))
Theorem	norm0 9003	The norm of a zero vector.
|- (normh` 0h) = 0
Theorem	norm-it 9004	Theorem 3.3(i) of [Beran] p. 97.
|- (A e. H~ -> ((normh` A) = 0 <-> A = 0h))
Theorem	normne0t 9005	A norm is nonzero iff its argument is a nonzero vector.
|- (A e. H~ -> ((normh` A) =/= 0 <-> A =/= 0h))
Theorem	normcl 9006	Real closure of the norm of a vector.
|- A e. H~   =>   |- (normh` A) e. RR
Theorem	normsq 9007	The square of a norm.
|- A e. H~   =>   |- ((normh` A)^2) = (A .ih A)
Theorem	norm-i 9008	Theorem 3.3(i) of [Beran] p. 97.
|- A e. H~   =>   |- ((normh` A) = 0 <-> A = 0h)
Theorem	normsqt 9009	The square of a norm.
|- (A e. H~ -> ((normh` A)^2) = (A .ih A))
Theorem	normsub0 9010	Two vectors are equal iff the norm of their difference is zero.
|- A e. H~   &   |- B e. H~   =>   |- ((normh` (A -h B)) = 0 <-> A = B)
Theorem	normsub0t 9011	Two vectors are equal iff the norm of their difference is zero.
|- ((A e. H~ /\ B e. H~) -> ((normh` (A -h B)) = 0 <-> A = B))
Theorem	norm-ii 9012	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97.
|- A e. H~   &   |- B e. H~   =>   |- (normh` (A +h B)) <_ ((normh` A) + (normh` B))
Theorem	norm-iit 9013	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97.
|- ((A e. H~ /\ B e. H~) -> (normh` (A +h B)) <_ ((normh` A) + (normh` B)))
Theorem	norm-iii 9014	Theorem 3.3(iii) of [Beran] p. 97.
|- A e. CC   &   |- B e. H~   =>   |- (normh` (A .h B)) = ((abs` A) x. (normh` B))
Theorem	norm-iiit 9015	Theorem 3.3(iii) of [Beran] p. 97.
|- ((A e. CC /\ B e. H~) -> (normh` (A .h B)) = ((abs` A) x. (normh` B)))
Theorem	normsub 9016	Negative doesn't change the norm of a Hilbert space vector.
|- A e. H~   &   |- B e. H~   =>   |- (normh` (A -h B)) = (normh` (B -h A))
Theorem	normpyth 9017	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98.
|- A e. H~   &   |- B e. H~   =>   |- ((A .ih B) = 0 -> ((normh` (A +h B))^2) = (((normh` A)^2) + ((normh` B)^2)))
Theorem	normsubt 9018	Swapping order of subtraction doesn't change the norm of a vector.
|- ((A e. H~ /\ B e. H~) -> (normh` (A -h B)) = (normh` (B -h A)))
Theorem	normnegt 9019	The norm of a vector equals the norm of its negative.
|- (A e. H~ -> (normh` (-u1 .h A)) = (normh` A))
Theorem	normpytht 9020	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98.
|- ((A e. H~ /\ B e. H~) -> ((A .ih B) = 0 -> ((normh` (A +h B))^2) = (((normh` A)^2) + ((normh` B)^2))))
Theorem	normpyct 9021	Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98.
|- ((A e. H~ /\ B e. H~) -> ((A .ih B) = 0 -> (normh` A) <_ (normh` (A +h B))))
Theorem	norm3dif 9022	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- (normh` (A -h B)) <_ ((normh` (A -h C)) + (normh` (C -h B)))
Theorem	norm3adif 9023	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- (abs` ((normh` (A -h C)) - (normh` (B -h C)))) <_ (normh` (A -h B))
Theorem	norm3lem 9024	Lemma involving norm of differences in Hilbert space.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. RR   =>   |- (((normh` (A -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) -> (normh` (A -h B)) < D)
Theorem	norm3dift 9025	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (normh` (A -h B)) <_ ((normh` (A -h C)) + (normh` (C -h B))))
Theorem	norm3dif2t 9026	Norm of differences around common element.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (normh` (A -h B)) <_ ((normh` (C -h A)) + (normh` (C -h B))))
Theorem	norm3lemt 9027	Lemma involving norm of differences in Hilbert space.
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. RR)) -> (((normh` (A -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) -> (normh` (A -h B)) < D))
Theorem	norm3adift 9028	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101.
|- C e. H~   =>   |- ((A e. H~ /\ B e. H~) -> (abs` ((normh` (A -h C)) - (normh` (B -h C)))) <_ (normh` (A -h B)))
Theorem	normpar 9029	Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98.
|- A e. H~   &   |- B e. H~   =>   |- (((normh` (A -h B))^2) + ((normh` (A +h B))^2)) = ((2 x. ((normh` A)^2)) + (2 x. ((normh` B)^2)))
Theorem	normpart 9030	Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98.
|- ((A e. H~ /\ B e. H~) -> (((normh` (A -h B))^2) + ((normh` (A +h B))^2)) = ((2 x. ((normh` A)^2)) + (2 x. ((normh` B)^2))))
Theorem	normpar2 9031	Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((normh` (A -h B))^2) = (((2 x. ((normh` (A -h C))^2)) + (2 x. ((normh` (B -h C))^2))) - ((normh` ((A +h B) -h (2 .h C)))^2))
Theorem	polid2 9032	Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. H~   =>   |- (A .ih B) = (((((A +h C) .ih (D +h B)) - ((A -h C) .ih (D -h B))) + (i x. (((A +h (i .h C)) .ih (D +h (i .h B))) - ((A -h (i .h C)) .ih (D -h (i .h B)))))) / 4)
Theorem	polid 9033	Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of axiom ax-his3 8959.
|- A e. H~   &   |- B e. H~   =>   |- (A .ih B) = (((((normh` (A +h B))^2) - ((normh` (A -h B))^2)) + (i x. (((normh` (A +h (i .h B)))^2) - ((normh` (A -h (i .h B)))^2)))) / 4)
Theorem	polidt 9034	Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of axiom ax-his3 8959.
|- ((A e. H~ /\ B e. H~) -> (A .ih B) = (((((normh` (A +h B))^2) - ((normh` (A -h B))^2)) + (i x. (((normh` (A +h (i .h B)))^2) - ((normh` (A -h (i .h B)))^2)))) / 4))
Relate Hilbert space to normed complex vector spaces
Theorem	hilabl 9035	Hilbert space vector addition is an Abelian group operation.
|- +h e. Abel
Theorem	hilid 9036	The group identity element of Hilbert space vector addition is the zero vector.
|- (Id` +h ) = 0h
Theorem	hilvc 9037	Hilbert space is a complex vector space. Vector addition is +h, and scalar product is .h.
|- <. +h , .h >. e. CVec
Theorem	hilnorm 9038	Hilbert space norm in terms of vector space norm.
|- H~ = (Base` U)   &   |- .ih = (.i` U)   &   |- U e. NrmCVec   =>   |- normh = (norm` U)
Theorem	hilhh 9039	Deduce the structure of Hilbert space from its components.
|- H~ = (Base` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- U e. NrmCVec   =>   |- U = <.<. +h , .h >., normh>.
Theorem	hhnv 9040	Hilbert space is a normed complex vector space.
|- U = <.<. +h , .h >., normh>.   =>