mmtheorems93 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 9201-9300 - Page 93 of 123

Type	Label	Description
Statement
Theorem	hvsubsub4i 9201	Hilbert vector space addition law.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. H~   =>   |- ((A -h B) -h (C -h D)) = ((A -h C) -h (B -h D))
Theorem	hvsubsub4 9202	Hilbert vector space addition/subtraction law.
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A -h B) -h (C -h D)) = ((A -h C) -h (B -h D)))
Theorem	hv2times 9203	Two times a vector.
|- (A e. H~ -> (2 .h A) = (A +h A))
Theorem	hvnegdii 9204	Distribution of negative over subtraction.
|- A e. H~   &   |- B e. H~   =>   |- (-u1 .h (A -h B)) = (B -h A)
Theorem	hvsubeq0i 9205	If the difference between two vectors is zero, they are equal.
|- A e. H~   &   |- B e. H~   =>   |- ((A -h B) = 0h <-> A = B)
Theorem	hvsubcan2i 9206	Vector cancellation law.
|- A e. H~   &   |- B e. H~   =>   |- ((A +h B) +h (A -h B)) = (2 .h A)
Theorem	hvaddcani 9207	Cancellation law for vector addition.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A +h B) = (A +h C) <-> B = C)
Theorem	hvsubaddi 9208	Relationship between vector subtraction and addition.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A -h B) = C <-> (B +h C) = A)
Theorem	hvnegdi 9209	Distribution of negative over subtraction.
|- ((A e. H~ /\ B e. H~) -> (-u1 .h (A -h B)) = (B -h A))
Theorem	hvsubeq0 9210	If the difference between two vectors is zero, they are equal.
|- ((A e. H~ /\ B e. H~) -> ((A -h B) = 0h <-> A = B))
Theorem	hvaddeq0 9211	If the sum of two vectors is zero, one is the negative of the other.
|- ((A e. H~ /\ B e. H~) -> ((A +h B) = 0h <-> A = (-u1 .h B)))
Theorem	hvaddcan 9212	Cancellation law for vector addition.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) = (A +h C) <-> B = C))
Theorem	hvaddcan2 9213	Cancellation law for vector addition.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h C) = (B +h C) <-> A = B))
Theorem	hvmulcan 9214	Cancellation law for scalar multiplication.
|- (((A e. CC /\ A =/= 0) /\ B e. H~ /\ C e. H~) -> ((A .h B) = (A .h C) <-> B = C))
Theorem	hvmulcanOLD 9215	Cancellation law for scalar multiplication.
|- (((A e. CC /\ B e. H~ /\ C e. H~) /\ A =/= 0) -> ((A .h B) = (A .h C) <-> B = C))
Theorem	hvmulcan2 9216	Cancellation law for scalar multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. H~ /\ C =/= 0h)) -> ((A .h C) = (B .h C) <-> A = B))
Theorem	hvsubcan 9217	Cancellation law for vector addition.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A -h B) = (A -h C) <-> B = C))
Theorem	hvsubcan2 9218	Cancellation law for vector addition.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A -h C) = (B -h C) <-> A = B))
Theorem	hvsub0 9219	Subtraction of a zero vector.
|- (A e. H~ -> (A -h 0h) = A)
Theorem	hvsubadd 9220	Relationship between vector subtraction and addition.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A -h B) = C <-> (B +h C) = A))
Theorem	hvaddsub4 9221	Hilbert vector space addition/subtraction law.
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A +h B) = (C +h D) <-> (A -h C) = (D -h B)))
Inner product postulates for a Hilbert space
Axiom	ax-hfi 9222	Inner product maps pairs from H~ to CC.
|- .ih :(H~ X. H~)-->CC
Theorem	hicl 9223	Closure of inner product.
|- ((A e. H~ /\ B e. H~) -> (A .ih B) e. CC)
Theorem	hicli 9224	Closure inference for inner product.
|- A e. H~   &   |- B e. H~   =>   |- (A .ih B) e. CC
Axiom	ax-his1 9225	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that *` x is the complex conjugate cjval 6964 of x. In the literature, the inner product of A and B is usually written <.A, B>., but our operation notation co 4021 allows us to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 2474. Physicists use <.B | A>., called Dirac bra-ket notation, to represent this operation; see comments in df-bra 10056.
|- ((A e. H~ /\ B e. H~) -> (A .ih B) = (*` (B .ih A)))
Axiom	ax-his2 9226	Distributive law for inner product. Postulate (S2) of [Beran] p. 95.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) .ih C) = ((A .ih C) + (B .ih C)))
Axiom	ax-his3 9227	Associative law for inner product. Postulate (S3) of [Beran] p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with (B .ih (A .h C)) (e.g. Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 10056 for why the physics definition is swapped.
|- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .h B) .ih C) = (A x. (B .ih C)))
Axiom	ax-his4 9228	Identity law for inner product. Postulate (S4) of [Beran] p. 95.
|- ((A e. H~ /\ A =/= 0h) -> 0 < (A .ih A))
Inner product
Theorem	his5 9229	Associative law for inner product. Lemma 3.1(S5) of [Beran] p. 95.
|- ((A e. CC /\ B e. H~ /\ C e. H~) -> (B .ih (A .h C)) = ((*` A) x. (B .ih C)))
Theorem	his52 9230	Associative law for inner product.
|- ((A e. CC /\ B e. H~ /\ C e. H~) -> (B .ih ((*` A) .h C)) = (A x. (B .ih C)))
Theorem	his35i 9231	Move scalar multiplication to outside of inner product.
|- A e. CC   &   |- B e. CC   &   |- C e. H~   &   |- D e. H~   =>   |- ((A .h C) .ih (B .h D)) = ((A x. (*` B)) x. (C .ih D))
Theorem	his7 9232	Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A .ih (B +h C)) = ((A .ih B) + (A .ih C)))
Theorem	hiassdi 9233	Distributive/associative law for inner product, useful for linearity proofs.
|- (((A e. CC /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> (((A .h B) +h C) .ih D) = ((A x. (B .ih D)) + (C .ih D)))
Theorem	his2sub 9234	Distributive law for inner product of vector subtraction.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A -h B) .ih C) = ((A .ih C) - (B .ih C)))
Theorem	his2sub2 9235	Distributive law for inner product of vector subtraction.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A .ih (B -h C)) = ((A .ih B) - (A .ih C)))
Theorem	hire 9236	A necessary and sufficient condition for an inner product to be real.
|- ((A e. H~ /\ B e. H~) -> ((A .ih B) e. RR <-> (A .ih B) = (B .ih A)))
Theorem	hiidrcl 9237	Real closure of inner product with self.
|- (A e. H~ -> (A .ih A) e. RR)
Theorem	hi01 9238	Inner product with the 0 vector.
|- (A e. H~ -> (0h .ih A) = 0)
Theorem	hi02 9239	Inner product with the 0 vector.
|- (A e. H~ -> (A .ih 0h) = 0)
Theorem	hiidge0 9240	Inner product with self is not negative.
|- (A e. H~ -> 0 <_ (A .ih A))
Theorem	his6 9241	Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95.
|- (A e. H~ -> ((A .ih A) = 0 <-> A = 0h))
Theorem	his1i 9242	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95.
|- A e. H~   &   |- B e. H~   =>   |- (A .ih B) = (*` (B .ih A))
Theorem	abshicom 9243	Commuted inner products have the same absolute values.
|- ((A e. H~ /\ B e. H~) -> (abs` (A .ih B)) = (abs` (B .ih A)))
Theorem	hial0 9244	A vector whose inner product is always zero is zero.
|- (A e. H~ -> (A.x e. H~ (A .ih x) = 0 <-> A = 0h))
Theorem	hial02 9245	A vector whose inner product is always zero is zero.
|- (A e. H~ -> (A.x e. H~ (x .ih A) = 0 <-> A = 0h))
Theorem	hisubcomi 9246	Two vector subtractions simultaneously commute in an inner product.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. H~   =>   |- ((A -h B) .ih (C -h D)) = ((B -h A) .ih (D -h C))
Theorem	hi2eq 9247	Lemma used to prove equality of vectors.
|- ((A e. H~ /\ B e. H~) -> ((A .ih (A -h B)) = (B .ih (A -h B)) <-> A = B))
Theorem	hial2eq 9248	Two vectors whose inner product is always equal are equal.
|- ((A e. H~ /\ B e. H~) -> (A.x e. H~ (A .ih x) = (B .ih x) <-> A = B))
Theorem	hial2eq2 9249	Two vectors whose inner product is always equal are equal.
|- ((A e. H~ /\ B e. H~) -> (A.x e. H~ (x .ih A) = (x .ih B) <-> A = B))
Theorem	orthcom 9250	Orthogonality commutes.
|- ((A e. H~ /\ B e. H~) -> ((A .ih B) = 0 <-> (B .ih A) = 0))
Theorem	normlem0 9251	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   =>   |- ((F -h (S .h G)) .ih (F -h (S .h G))) = (((F .ih F) + (-u(*` S) x. (F .ih G))) + ((-uS x. (G .ih F)) + ((S x. (*` S)) x. (G .ih G))))
Theorem	normlem1 9252	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   &   |- R e. RR   &   |- (abs` S) = 1   =>   |- ((F -h ((S x. R) .h G)) .ih (F -h ((S x. R) .h G))) = (((F .ih F) + (((*` S) x. -uR) x. (F .ih G))) + (((S x. -uR) x. (G .ih F)) + ((R^2) x. (G .ih G))))
Theorem	normlem2 9253	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   &   |- B = -u(((*` S) x. (F .ih G)) + (S x. (G .ih F)))   =>   |- B e. RR
Theorem	normlem3 9254	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   &   |- B = -u(((*` S) x. (F .ih G)) + (S x. (G .ih F)))   &   |- A = (G .ih G)   &   |- C = (F .ih F)   &   |- R e. RR   =>   |- (((A x. (R^2)) + (B x. R)) + C) = (((F .ih F) + (((*` S) x. -uR) x. (F .ih G))) + (((S x. -uR) x. (G .ih F)) + ((R^2) x. (G .ih G))))
Theorem	normlem4 9255	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   &   |- B = -u(((*` S) x. (F .ih G)) + (S x. (G .ih F)))   &   |- A = (G .ih G)   &   |- C = (F .ih F)   &   |- R e. RR   &   |- (abs` S) = 1   =>   |- ((F -h ((S x. R) .h G)) .ih (F -h ((S x. R) .h G))) = (((A x. (R^2)) + (B x. R)) + C)
Theorem	normlem5 9256	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   &   |- B = -u(((*` S) x. (F .ih G)) + (S x. (G .ih F)))   &   |- A = (G .ih G)   &   |- C = (F .ih F)   &   |- R e. RR   &   |- (abs` S) = 1   =>   |- 0 <_ (((A x. (R^2)) + (B x. R)) + C)
Theorem	normlem6 9257	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   &   |- B = -u(((*` S) x. (F .ih G)) + (S x. (G .ih F)))   &   |- A = (G .ih G)   &   |- C = (F .ih F)   &   |- (abs` S) = 1   =>   |- (abs` B) <_ (2 x. ((sqr` A) x. (sqr` C)))
Theorem	normlem7 9258	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- S e. CC   &   |- F e. H~   &   |- G e. H~   &   |- (abs` S) = 1   =>   |- (((*` S) x. (F .ih G)) + (S x. (G .ih F))) <_ (2 x. ((sqr` (G .ih G)) x. (sqr` (F .ih F))))
Theorem	normlem8 9259	Lemma used to derive properties of norm.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. H~   =>   |- ((A +h B) .ih (C +h D)) = (((A .ih C) + (B .ih D)) + ((A .ih D) + (B .ih C)))
Theorem	normlem9 9260	Lemma used to derive properties of norm.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. H~   =>   |- ((A -h B) .ih (C -h D)) = (((A .ih C) + (B .ih D)) - ((A .ih D) + (B .ih C)))
Theorem	normlem7tALT 9261	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
|- A e. H~   &   |- B e. H~   =>   |- ((S e. CC /\ (abs` S) = 1) -> (((*` S) x. (A .ih B)) + (S x. (B .ih A))) <_ (2 x. ((sqr` (B .ih B)) x. (sqr` (A .ih A)))))
Theorem	bcseqi 9262	Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 9323.
|- A e. H~   &   |- B e. H~   =>   |- (((A .ih B) x. (B .ih A)) = ((A .ih A) x. (B .ih B)) <-> ((B .ih B) .h A) = ((A .ih B) .h B))
Theorem	normlem9at 9263	Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98.
|- ((A e. H~ /\ B e. H~) -> ((A -h B) .ih (A -h B)) = (((A .ih A) + (B .ih B)) - ((A .ih B) + (B .ih A))))
Norms
Theorem	dfhnorm2 9264	Alternate definition of the norm of a vector of Hilbert space. Definition of norm in [Beran] p. 96.
|- normh = {<.x, y>. | (x e. H~ /\ y = (sqr` (x .ih x)))}
Theorem	normf 9265	The norm function maps from Hilbert space to reals.
|- normh:H~-->RR
Theorem	normval 9266	The value of the norm of a vector in Hilbert space. Definition of norm in [Beran] p. 96. In the literature, the norm of A is usually written as "|| A ||", but we use function value notation to take advantage of our existing theorems about functions.
|- (A e. H~ -> (normh` A) = (sqr` (A .ih A)))
Theorem	normcl 9267	Real closure of the norm of a vector.
|- (A e. H~ -> (normh` A) e. RR)
Theorem	normge0 9268	The norm of a vector is nonnegative.
|- (A e. H~ -> 0 <_ (normh` A))
Theorem	normgt0OLD 9269	The norm of non-zero vector is positive.
|- (A e. H~ -> (-. A = 0h <-> 0 < (normh` A)))
Theorem	normgt0 9270	The norm of non-zero vector is positive.
|- (A e. H~ -> (A =/= 0h <-> 0 < (normh` A)))
Theorem	norm0 9271	The norm of a zero vector.
|- (normh` 0h) = 0
Theorem	norm-i 9272	Theorem 3.3(i) of [Beran] p. 97.
|- (A e. H~ -> ((normh` A) = 0 <-> A = 0h))
Theorem	normne0 9273	A norm is nonzero iff its argument is a nonzero vector.
|- (A e. H~ -> ((normh` A) =/= 0 <-> A =/= 0h))
Theorem	normcli 9274	Real closure of the norm of a vector.
|- A e. H~   =>   |- (normh` A) e. RR
Theorem	normsqi 9275	The square of a norm.
|- A e. H~   =>   |- ((normh` A)^2) = (A .ih A)
Theorem	norm-i.i 9276	Theorem 3.3(i) of [Beran] p. 97.
|- A e. H~   =>   |- ((normh` A) = 0 <-> A = 0h)
Theorem	normsq 9277	The square of a norm.
|- (A e. H~ -> ((normh` A)^2) = (A .ih A))
Theorem	normsub0i 9278	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	normsub0 9279	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.i 9280	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-ii 9281	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.i 9282	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-iii 9283	Theorem 3.3(iii) of [Beran] p. 97.
|- ((A e. CC /\ B e. H~) -> (normh` (A .h B)) = ((abs` A) x. (normh` B)))
Theorem	normsubi 9284	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	normpythi 9285	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	normsub 9286	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	normneg 9287	The norm of a vector equals the norm of its negative.
|- (A e. H~ -> (normh` (-u1 .h A)) = (normh` A))
Theorem	normpyth 9288	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	normpyc 9289	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	norm3difi 9290	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	norm3adifii 9291	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 9292	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	norm3dif 9293	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	norm3dif2 9294	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 9295	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	norm3adifi 9296	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	normpari 9297	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	normpar 9298	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	normpar2i 9299	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	polid2i 9300	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)