Metamath Proof Explorer - mmtheorems51

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 5001-5100 - Page 51 of 58

Type	Label	Description
Statement
Theorem	hvsubval 5001	Value of vector subtraction definition.
|- A e. H~   &   |- B e. H~   =>   |- (A -v B) = (A +v (-u1 .s B))
Theorem	hvsubcl 5002	Closure of vector subtraction.
|- A e. H~   &   |- B e. H~   =>   |- (A -v B) e. H~
Theorem	hvaddid2t 5003	Addition with the zero vector.
|- (A e. H~ -> (0v +v A) = A)
Theorem	hvmul0t 5004	Scalar multiplication with the zero vector.
|- (A e. CC -> (A .s 0v) = 0v)
Theorem	hvsubidt 5005	Subtraction of a vector from itself.
|- (A e. H~ -> (A -v A) = 0v)
Theorem	hvnegidt 5006	Addition of negative of a vector to itself.
|- (A e. H~ -> (A +v (-u1 .s A)) = 0v)
Theorem	hvm1negt 5007	Convert minus one times a scalar product to the negative of the scalar.
|- ((A e. CC /\ B e. H~) -> (-u1 .s (A .s B)) = (-uA .s B))
Theorem	hvaddid2 5008	Addition with the zero vector.
|- A e. H~   =>   |- (0v +v A) = A
Theorem	hvnegid 5009	Addition of negative of a vector to itself.
|- A e. H~   =>   |- (A +v (-u1 .s A)) = 0v
Theorem	hv2neg 5010	Two ways of expressing negative.
|- A e. H~   =>   |- (0v -v A) = (-u1 .s A)
Theorem	hvadd23t 5011	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +v B) +v C) = ((A +v C) +v B))
Theorem	hvadd12t 5012	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A +v (B +v C)) = (B +v (A +v C)))
Theorem	hvadd4t 5013	Hilbert vector space addition law.
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A +v B) +v (C +v D)) = ((A +v C) +v (B +v D)))
Theorem	hvsub4t 5014	Hilbert vector space addition/subtraction law.
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A +v B) -v (C +v D)) = ((A -v C) +v (B -v D)))
Theorem	hvaddsub12t 5015	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A +v (B -v C)) = (B +v (A -v C)))
Theorem	hvsubcan1t 5016	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. H~ /\ B e. H~) -> ((A +v B) -v B) = A)
Theorem	hvsubcan2t 5017	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. H~ /\ B e. H~) -> ((A +v B) -v A) = B)
Theorem	hvaddsubasst 5018	Associativity of sum and difference of Hilbert space vectors.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +v B) -v C) = (A +v (B -v C)))
Theorem	hvsubaddeqt 5019	Subtraction and addition of equal Hilbert space vectors..
|- ((A e. H~ /\ B e. H~) -> (A +v (B -v A)) = B)
Theorem	hvmulass 5020	Scalar multiplication associative law.
|- A e. CC   &   |- B e. CC   &   |- C e. H~   =>   |- ((A x. B) .s C) = (A .s (B .s C))
Theorem	hvmulcom 5021	Scalar multiplication commutative law.
|- A e. CC   &   |- B e. CC   &   |- C e. H~   =>   |- (A .s (B .s C)) = (B .s (A .s C))
Theorem	hvmul2neg 5022	Double negative in scalar multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. H~   =>   |- (-uA .s (-uB .s C)) = (A .s (B .s C))
Theorem	hvdistr1 5023	Scalar multiplication distributive law.
|- A e. CC   &   |- B e. H~   &   |- C e. H~   =>   |- (A .s (B +v C)) = ((A .s B) +v (A .s C))
Theorem	hvsubdistr1 5024	Scalar multiplication distributive law.
|- A e. CC   &   |- B e. H~   &   |- C e. H~   =>   |- (A .s (B -v C)) = ((A .s B) -v (A .s C))
Theorem	hvass 5025	Hilbert vector space associative law.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A +v B) +v C) = (A +v (B +v C))
Theorem	hvadd23 5026	Hilbert vector space commutative/associative law.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A +v B) +v C) = ((A +v C) +v B)
Theorem	hvsubass 5027	Hilbert vector space associative law for subtraction.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A -v B) -v C) = (A -v (B +v C))
Theorem	hvsub23 5028	Hilbert vector space commutative/associative law.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A -v B) -v C) = ((A -v C) -v B)
Theorem	hvadd12 5029	Hilbert vector space commutative/associative law.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- (A +v (B +v C)) = (B +v (A +v C))
Theorem	hvadd4 5030	Hilbert vector space addition law.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. H~   =>   |- ((A +v B) +v (C +v D)) = ((A +v C) +v (B +v D))
Theorem	hvsubsub4 5031	Hilbert vector space addition law.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   &   |- D e. H~   =>   |- ((A -v B) -v (C -v D)) = ((A -v C) -v (B -v D))
Theorem	hvsubsub4t 5032	Hilbert vector space addition/subtraction law.
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A -v B) -v (C -v D)) = ((A -v C) -v (B -v D)))
Theorem	hv2times 5033	Two times a vector.
|- A e. H~   =>   |- (2 .s A) = (A +v A)
Theorem	hvnegdi 5034	Distribution of negative over subtraction.
|- A e. H~   &   |- B e. H~   =>   |- (-u1 .s (A -v B)) = (B -v A)
Theorem	hvsubeq0 5035	If the difference between two vectors is zero, they are equal.
|- A e. H~   &   |- B e. H~   =>   |- ((A -v B) = 0v <-> A = B)
Theorem	hvsubcan2 5036	Vector cancellation law.
|- A e. H~   &   |- B e. H~   =>   |- ((A +v B) +v (A -v B)) = (2 .s A)
Theorem	hvaddcan 5037	Cancellation law for vector addition.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A +v B) = (A +v C) <-> B = C)
Theorem	hvsubadd 5038	Relationship between vector subtraction and addition.
|- A e. H~   &   |- B e. H~   &   |- C e. H~   =>   |- ((A -v B) = C <-> (B +v C) = A)
Theorem	hvnegdit 5039	Distribution of negative over subtraction.
|- ((A e. H~ /\ B e. H~) -> (-u1 .s (A -v B)) = (B -v A))
Theorem	hvsubeq0t 5040	If the difference between two vectors is zero, they are equal.
|- ((A e. H~ /\ B e. H~) -> ((A -v B) = 0v <-> A = B))
Theorem	hvsub0t 5041	Subtraction of a zero vector.
|- (A e. H~ -> (A -v 0v) = A)
Theorem	hvsubaddt 5042	Relationship between vector subtraction and addition.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A -v B) = C <-> (B +v C) = A))
Axiom	ax-hicl 5043	Closure of inner product.
|- ((A e. H~ /\ B e. H~) -> (A .i B) e. CC)
Theorem	hicl 5044	Closure inference for inner product.
|- A e. H~   &   |- B e. H~   =>   |- (A .i B) e. CC
Axiom	ax-his1 5045	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that *` x is the complex conjugate cjvalt 4799 of x. In the literature, the inner product of A and B is usually written <.A, B>. but our operation notation allows us to use existing theorems about operations and also eliminates ambiguity with the definition of an ordered pair df-op 1815.
|- ((A e. H~ /\ B e. H~) -> (A .i B) = (*` (B .i A)))
Axiom	ax-his2 5046	Distributive law for inner product. Postulate (S2) of [Beran] p. 95.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +v B) .i C) = ((A .i C) + (B .i C)))
Axiom	ax-his3 5047	Associative law for inner product. Postulate (S3) of [Beran] p. 95.
|- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .s B) .i C) = (A x. (B .i C)))
Axiom	ax-his4 5048	Identity law for inner product. Postulate (S4) of [Beran] p. 95.
|- ((A e. H~ /\ A =/= 0v) -> 0 < (A .i A))
Theorem	axhis42 5049	Identity law for inner product. Postulate (S4) of [Beran] p. 95.
|- ((A e. H~ /\ -. A = 0v) -> 0 < (A .i A))
Theorem	his5 5050	Associative law for inner product. Lemma 3.1(S5) of [Beran] p. 95.
|- ((A e. CC /\ B e. H~ /\ C e. H~) -> (B .i (A .s C)) = ((*` A) x. (B .i C)))
Theorem	his7 5051	Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A .i (B +v C)) = ((A .i B) + (A .i C)))
Theorem	his2subt 5052	Distributive law for inner product of vector subtraction.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A -v B) .i C) = ((A .i C) - (B .i C)))
Theorem	hiidrclt 5053	Real closure of inner product with self.
|- (A e. H~ -> (A .i A) e. RR)
Theorem	hizer1t 5054	Inner product with the 0 vector.
|- (A e. H~ -> (0v .i A) = 0)
Theorem	hizer2t 5055	Inner product with the 0 vector.
|- (A e. H~ -> (A .i 0v) = 0)
Theorem	hiidge0t 5056	Inner product with self is not negative.
|- (A e. H~ -> 0 <_ (A .i A))
Theorem	his6 5057	Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95.
|- (A e. H~ ->