P. 280 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27901-28000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hvsubass 27901	Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( A -h ( B +h C ) ) )
Theorem	hvsub32 27902	Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( ( A -h C ) -h B ) )
Theorem	hvmulassi 27903	Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- A e. CC   &    |- B e. CC   &    |- C e. ~H   =>    |- ( ( A x. B ) .h C ) = ( A .h ( B .h C ) )
Theorem	hvmulcomi 27904	Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- A e. CC   &    |- B e. CC   &    |- C e. ~H   =>    |- ( A .h ( B .h C ) ) = ( B .h ( A .h C ) )
Theorem	hvmul2negi 27905	Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- A e. CC   &    |- B e. CC   &    |- C e. ~H   =>    |- ( -u A .h ( -u B .h C ) ) = ( A .h ( B .h C ) )
Theorem	hvsubdistr1 27906	Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B -h C ) ) = ( ( A .h B ) -h ( A .h C ) ) )
Theorem	hvsubdistr2 27907	Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A - B ) .h C ) = ( ( A .h C ) -h ( B .h C ) ) )
Theorem	hvdistr1i 27908	Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- A e. CC   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) )
Theorem	hvsubdistr1i 27909	Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- A e. CC   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( A .h ( B -h C ) ) = ( ( A .h B ) -h ( A .h C ) )
Theorem	hvassi 27910	Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( ( A +h B ) +h C ) = ( A +h ( B +h C ) )
Theorem	hvadd32i 27911	Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( ( A +h B ) +h C ) = ( ( A +h C ) +h B )
Theorem	hvsubassi 27912	Hilbert vector space associative law for subtraction. (Contributed by NM, 7-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( ( A -h B ) -h C ) = ( A -h ( B +h C ) )
Theorem	hvsub32i 27913	Hilbert vector space commutative/associative law. (Contributed by NM, 7-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( ( A -h B ) -h C ) = ( ( A -h C ) -h B )
Theorem	hvadd12i 27914	Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( A +h ( B +h C ) ) = ( B +h ( A +h C ) )
Theorem	hvadd4i 27915	Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- 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	hvsubsub4i 27916	Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- 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 27917	Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
|- ( ( ( 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 27918	Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( 2 .h A ) = ( A +h A ) )
Theorem	hvnegdii 27919	Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( -u 1 .h ( A -h B ) ) = ( B -h A )
Theorem	hvsubeq0i 27920	If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( ( A -h B ) = 0h <-> A = B )
Theorem	hvsubcan2i 27921	Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( ( A +h B ) +h ( A -h B ) ) = ( 2 .h A )
Theorem	hvaddcani 27922	Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( ( A +h B ) = ( A +h C ) <-> B = C )
Theorem	hvsubaddi 27923	Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. ~H   =>    |- ( ( A -h B ) = C <-> ( B +h C ) = A )
Theorem	hvnegdi 27924	Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( -u 1 .h ( A -h B ) ) = ( B -h A ) )
Theorem	hvsubeq0 27925	If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A -h B ) = 0h <-> A = B ) )
Theorem	hvaddeq0 27926	If the sum of two vectors is zero, one is the negative of the other. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) = 0h <-> A = ( -u 1 .h B ) ) )
Theorem	hvaddcan 27927	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h B ) = ( A +h C ) <-> B = C ) )
Theorem	hvaddcan2 27928	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h C ) = ( B +h C ) <-> A = B ) )
Theorem	hvmulcan 27929	Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) = ( A .h C ) <-> B = C ) )
Theorem	hvmulcan2 27930	Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( A .h C ) = ( B .h C ) <-> A = B ) )
Theorem	hvsubcan 27931	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) = ( A -h C ) <-> B = C ) )
Theorem	hvsubcan2 27932	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h C ) = ( B -h C ) <-> A = B ) )
Theorem	hvsub0 27933	Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
|- ( A e. ~H -> ( A -h 0h ) = A )
Theorem	hvsubadd 27934	Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) = C <-> ( B +h C ) = A ) )
Theorem	hvaddsub4 27935	Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) = ( C +h D ) <-> ( A -h C ) = ( D -h B ) ) )
19.1.6  Inner product postulates for a Hilbert space
Axiom	ax-hfi 27936	Inner product maps pairs from ~H to CC. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
|- .ih : ( ~H X. ~H ) --> CC
Theorem	hicl 27937	Closure of inner product. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) e. CC )
Theorem	hicli 27938	Closure inference for inner product. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( A .ih B ) e. CC
Axiom	ax-his1 27939	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that * ` x is the complex conjugate cjval 13842 of x. In the literature, the inner product of A and B is usually written <. A , B >., but our operation notation co 6650 allows us to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4184. Physicists use <. B | A >., called Dirac bra-ket notation, to represent this operation; see comments in df-bra 28709. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )
Axiom	ax-his2 27940	Distributive law for inner product. Postulate (S2) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h B ) .ih C ) = ( ( A .ih C ) + ( B .ih C ) ) )
Axiom	ax-his3 27941	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 28709 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )
Axiom	ax-his4 27942	Identity law for inner product. Postulate (S4) of [Beran] p. 95. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )
19.2  Inner product and norms
19.2.1  Inner product
Theorem	his5 27943	Associative law for inner product. Lemma 3.1(S5) of [Beran] p. 95. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B .ih ( A .h C ) ) = ( ( * ` A ) x. ( B .ih C ) ) )
Theorem	his52 27944	Associative law for inner product. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B .ih ( ( * ` A ) .h C ) ) = ( A x. ( B .ih C ) ) )
Theorem	his35 27945	Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
|- ( ( ( 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	his35i 27946	Move scalar multiplication to outside of inner product. (Contributed by NM, 1-Jul-2005.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
|- 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 27947	Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih ( B +h C ) ) = ( ( A .ih B ) + ( A .ih C ) ) )
Theorem	hiassdi 27948	Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005.) (New usage is discouraged.)
|- ( ( ( 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 27949	Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) .ih C ) = ( ( A .ih C ) - ( B .ih C ) ) )
Theorem	his2sub2 27950	Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih ( B -h C ) ) = ( ( A .ih B ) - ( A .ih C ) ) )
Theorem	hire 27951	A necessary and sufficient condition for an inner product to be real. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) e. RR <-> ( A .ih B ) = ( B .ih A ) ) )
Theorem	hiidrcl 27952	Real closure of inner product with self. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( A .ih A ) e. RR )
Theorem	hi01 27953	Inner product with the 0 vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( 0h .ih A ) = 0 )
Theorem	hi02 27954	Inner product with the 0 vector. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( A .ih 0h ) = 0 )
Theorem	hiidge0 27955	Inner product with self is not negative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
|- ( A e. ~H -> 0 <_ ( A .ih A ) )
Theorem	his6 27956	Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( ( A .ih A ) = 0 <-> A = 0h ) )
Theorem	his1i 27957	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. (Contributed by NM, 15-May-2005.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( A .ih B ) = ( * ` ( B .ih A ) )
Theorem	abshicom 27958	Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( A .ih B ) ) = ( abs ` ( B .ih A ) ) )
Theorem	hial0 27959*	A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( A. x e. ~H ( A .ih x ) = 0 <-> A = 0h ) )
Theorem	hial02 27960*	A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( A. x e. ~H ( x .ih A ) = 0 <-> A = 0h ) )
Theorem	hisubcomi 27961	Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
|- 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 27962	Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) <-> A = B ) )
Theorem	hial2eq 27963*	Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( A .ih x ) = ( B .ih x ) <-> A = B ) )
Theorem	hial2eq2 27964*	Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( x .ih A ) = ( x .ih B ) <-> A = B ) )
Theorem	orthcom 27965	Orthogonality commutes. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) )
Theorem	normlem0 27966	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 7-Oct-1999.) (New usage is discouraged.)
|- 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 ) ) ) + ( ( -u S x. ( G .ih F ) ) + ( ( S x. ( * ` S ) ) x. ( G .ih G ) ) ) )
Theorem	normlem1 27967	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 22-Aug-1999.) (New usage is discouraged.)
|- 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. -u R ) x. ( F .ih G ) ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )
Theorem	normlem2 27968	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.)
|- 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 27969	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
|- 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. -u R ) x. ( F .ih G ) ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )
Theorem	normlem4 27970	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
|- 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 27971	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Aug-1999.) (New usage is discouraged.)
|- 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 27972	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) (New usage is discouraged.)
|- 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 27973	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
|- 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 27974	Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
|- 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 27975	Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
|- 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 27976	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
|- 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 27977	Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 28037. (Contributed by NM, 16-Jul-2001.) (New usage is discouraged.)
|- 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 27978	Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 10-May-2005.) (New usage is discouraged.)
|- ( ( 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 ) ) ) )
19.2.2  Norms
Theorem	dfhnorm2 27979	Alternate definition of the norm of a vector of Hilbert space. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- normh = ( x e. ~H |-> ( sqr ` ( x .ih x ) ) )
Theorem	normf 27980	The norm function maps from Hilbert space to reals. (Contributed by NM, 6-Sep-2007.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- normh : ~H --> RR
Theorem	normval 27981	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. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
|- ( A e. ~H -> ( normh ` A ) = ( sqr ` ( A .ih A ) ) )
Theorem	normcl 27982	Real closure of the norm of a vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( normh ` A ) e. RR )
Theorem	normge0 27983	The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
|- ( A e. ~H -> 0 <_ ( normh ` A ) )
Theorem	normgt0 27984	The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
Theorem	norm0 27985	The norm of a zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
|- ( normh ` 0h ) = 0
Theorem	norm-i 27986	Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( ( normh ` A ) = 0 <-> A = 0h ) )
Theorem	normne0 27987	A norm is nonzero iff its argument is a nonzero vector. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
Theorem	normcli 27988	Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.)
|- A e. ~H   =>    |- ( normh ` A ) e. RR
Theorem	normsqi 27989	The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
|- A e. ~H   =>    |- ( ( normh ` A ) ^ 2 ) = ( A .ih A )
Theorem	norm-i-i 27990	Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 5-Sep-1999.) (New usage is discouraged.)
|- A e. ~H   =>    |- ( ( normh ` A ) = 0 <-> A = 0h )
Theorem	normsq 27991	The square of a norm. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
|- ( A e. ~H -> ( ( normh ` A ) ^ 2 ) = ( A .ih A ) )
Theorem	normsub0i 27992	Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( ( normh ` ( A -h B ) ) = 0 <-> A = B )
Theorem	normsub0 27993	Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( normh ` ( A -h B ) ) = 0 <-> A = B ) )
Theorem	norm-ii-i 27994	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( normh ` ( A +h B ) ) <_ ( ( normh ` A ) + ( normh ` B ) )
Theorem	norm-ii 27995	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( normh ` ( A +h B ) ) <_ ( ( normh ` A ) + ( normh ` B ) ) )
Theorem	norm-iii-i 27996	Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
|- A e. CC   &    |- B e. ~H   =>    |- ( normh ` ( A .h B ) ) = ( ( abs ` A ) x. ( normh ` B ) )
Theorem	norm-iii 27997	Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. ~H ) -> ( normh ` ( A .h B ) ) = ( ( abs ` A ) x. ( normh ` B ) ) )
Theorem	normsubi 27998	Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( normh ` ( A -h B ) ) = ( normh ` ( B -h A ) )
Theorem	normpythi 27999	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( ( A .ih B ) = 0 -> ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) )
Theorem	normsub 28000	Swapping order of subtraction doesn't change the norm of a vector. (Contributed by NM, 14-Aug-1999.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( normh ` ( A -h B ) ) = ( normh ` ( B -h A ) ) )