mmtheorems89 - 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-10658

Statement List for Metamath Proof Explorer - 8801-8900 - Page 89 of 107

Type	Label	Description
Statement
Theorem	axhvmulass 8801	Derive axiom ax-hvmulass 8819 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- ((A e. CC /\ B e. CC /\ C e. H~) -> ((A x. B) .h C) = (A .h (B .h C)))
Theorem	axhvdistr1 8802	Derive axiom ax-hvdistr1 8820 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- ((A e. CC /\ B e. H~ /\ C e. H~) -> (A .h (B +h C)) = ((A .h B) +h (A .h C)))
Theorem	axhvdistr2 8803	Derive axiom ax-hvdistr2 8821 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- ((A e. CC /\ B e. CC /\ C e. H~) -> ((A + B) .h C) = ((A .h C) +h (B .h C)))
Theorem	axhvmul0 8804	Derive axiom ax-hvmul0 8822 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (0 .h A) = 0h)
Theorem	axhfi 8805	Derive axiom ax-hfi 8888 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- .ih :(H~ X. H~)-->CC
Theorem	axhis1 8806	Derive axiom ax-his1 8891 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. H~ /\ B e. H~) -> (A .ih B) = (*` (B .ih A)))
Theorem	axhis2 8807	Derive axiom ax-his2 8892 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) .ih C) = ((A .ih C) + (B .ih C)))
Theorem	axhis3 8808	Derive axiom ax-his3 8893 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .h B) .ih C) = (A x. (B .ih C)))
Theorem	axhis4 8809	Derive axiom ax-his4 8894 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. H~ /\ A =/= 0h) -> 0 < (A .ih A))
Theorem	axhcompl 8810	Derive axiom ax-hcompl 9013 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (F e. Cauchy -> E.x e. H~ F ~~>v x)
Introduce the vector space axioms for a Hilbert space
Axiom	ax-hilex 8811	This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. We assume that there exists a primitive class, H~, which contains objects called vectors. The 18 axioms for a complex Hilbert space consist of ax-hilex 8811, ax-hfvadd 8812, ax-hvcom 8813, ax-hvass 8814, ax-hv0cl 8815, ax-hvaddid 8816, ax-hfvmul 8817, ax-hvmulid 8818, ax-hvmulass 8819, ax-hvdistr1 8820, ax-hvdistr2 8821, ax-hvmul0 8822, ax-hfi 8888, ax-his1 8891, ax-his2 8892, ax-his3 8893, ax-his4 8894, and ax-hcompl 9013. The axioms specify the properties of 5 primitive symbols, H~, +h, .h, 0h, and .ih. If can prove in ZFC set theory that a class U = <.<. +h , .h >., normh>. is a complex Hilbert space, i.e. that U e. CHil, then these axioms can be proved as theorems axhilex 8793, axhfvadd 8794, axhvcom 8795, axhvass 8796, axhv0cl 8797, axhvaddid 8798 , axhfvmul 8799, axhvmulid 8800, axhvmulass 8801, axhvdistr1 8802, axhvdistr2 8803 , axhvmul0 8804, axhfi 8805, axhis1 8806, axhis2 8807, axhis3 8808, axhis4 8809, and axhcompl 8810 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 8793.
|- H~ e. V
Axiom	ax-hfvadd 8812	Vector addition is an operation on H~.
|- +h :(H~ X. H~)-->H~
Axiom	ax-hvcom 8813	Vector addition is commutative.
|- ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))
Axiom	ax-hvass 8814	Vector addition is associative.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) +h C) = (A +h (B +h C)))
Axiom	ax-hv0cl 8815	The zero vector is in the vector space.
|- 0h e. H~
Axiom	ax-hvaddid 8816	Addition with the zero vector.
|- (A e. H~ -> (A +h 0h) = A)
Axiom	ax-hfvmul 8817	Scalar multiplication is an operation on CC and H~.
|- .h :(CC X. H~)-->H~
Axiom	ax-hvmulid 8818	Scalar multiplication by one.
|- (A e. H~ -> (1 .h A) = A)
Axiom	ax-hvmulass 8819	Scalar multiplication associative law
|- ((A e. CC /\ B e. CC /\ C e. H~) -> ((A x. B) .h C) = (A .h (B .h C)))
Axiom	ax-hvdistr1 8820	Scalar multiplication distributive law
|- ((A e. CC /\ B e. H~ /\ C e. H~) -> (A .h (B +h C)) = ((A .h B) +h (A .h C)))
Axiom	ax-hvdistr2 8821	Scalar multiplication distributive law
|- ((A e. CC /\ B e. CC /\ C e. H~) -> ((A + B) .h C) = ((A .h C) +h (B .h C)))
Axiom	ax-hvmul0 8822	Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubidt 8837 and hvsubvalt 8828).
|- (A e. H~ -> (0 .h A) = 0h)
Vector operations
Theorem	hvmulex 8823	The Hilbert space scalar product operation is a set.
|- .h e. V
Theorem	hvaddclt 8824	Closure of vector addition.
|- ((A e. H~ /\ B e. H~) -> (A +h B) e. H~)
Theorem	hvmulclt 8825	Closure of scalar multiplication.
|- ((A e. CC /\ B e. H~) -> (A .h B) e. H~)
Theorem	hvmulcl 8826	Closure inference for scalar multiplication.
|- A e. CC   &   |- B e. H~   =>   |- (A .h B) e. H~
Theorem	hvsubopr 8827	Mapping domain and codomain of vector subtraction.
|- -h :(H~ X. H~)-->H~
Theorem	hvsubvalt 8828	Value of vector subtraction.
|- ((A e. H~ /\ B e. H~) -> (A -h B) = (A +h (-u1 .h B)))
Theorem	hvsubclt 8829	Closure of vector subtraction.
|- ((A e. H~ /\ B e. H~) -> (A -h B) e. H~)
Theorem	hvaddcl 8830	Closure of vector addition.
|- A e. H~   &   |- B e. H~   =>   |- (A +h B) e. H~
Theorem	hvcom 8831	Commutation of vector addition.
|- A e. H~   &   |- B e. H~   =>   |- (A +h B) = (B +h A)
Theorem	hvsubval 8832	Value of vector subtraction definition.
|- A e. H~   &   |- B e. H~   =>   |- (A -h B) = (A +h (-u1 .h B))
Theorem	hvsubcl 8833	Closure of vector subtraction.
|- A e. H~   &   |- B e. H~   =>   |- (A -h B) e. H~
Theorem	hvaddid2t 8834	Addition with the zero vector.
|- (A e. H~ -> (0h +h A) = A)
Theorem	hvmul0t 8835	Scalar multiplication with the zero vector.
|- (A e. CC -> (A .h 0h) = 0h)
Theorem	hvmul0ort 8836	If a scalar product is zero, one of its factors must be zero.
|- ((A e. CC /\ B e. H~) -> ((A .h B) = 0h <-> (A = 0 \/ B = 0h)))
Theorem	hvsubidt 8837	Subtraction of a vector from itself.
|- (A e. H~ -> (A -h A) = 0h)
Theorem	hvnegidt 8838	Addition of negative of a vector to itself.
|- (A e. H~ -> (A +h (-u1 .h A)) = 0h)
Theorem	hv2negt 8839	Two ways to express the negative of a vector.
|- (A e. H~ -> (0h -h A) = (-u1 .h A))
Theorem	hvaddid2 8840	Addition with the zero vector.
|- A e. H~   =>   |- (0h +h A) = A
Theorem	hvnegid 8841	Addition of negative of a vector to itself.
|- A e. H~   =>   |- (A +h (-u1 .h A)) = 0h
Theorem	hv2neg 8842	Two ways to express the negative of a vector.
|- A e. H~   =>   |- (0h -h A) = (-u1 .h A)
Theorem	hvm1negt 8843	Convert minus one times a scalar product to the negative of the scalar.
|- ((A e. CC /\ B e. H~) -> (-u1 .h (A .h B)) = (-uA .h B))
Theorem	hvaddsubvalt 8844	Value of vector addition in terms of vector subtraction.
|- ((A e. H~ /\ B e. H~) -> (A +h B) = (A -h (-u1 .h B)))
Theorem	hvadd23t 8845	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) +h C) = ((A +h C) +h B))
Theorem	hvadd12t 8846	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A +h (B +h C)) = (B +h (A +h C)))
Theorem	hvadd4t 8847	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	hvsub4t 8848	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	hvaddsub12t 8849	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A +h (B -h C)) = (B +h (A -h C)))
Theorem	hvpncant 8850	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. H~ /\ B e. H~) -> ((A +h B) -h B) = A)
Theorem	hvpncan2t 8851	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. H~ /\ B e. H~) -> ((A +h B) -h A) = B)
Theorem	hvaddsubasst 8852	Associativity of sum and difference of Hilbert space vectors.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) -h C) = (A +h (B -h C)))
Theorem	hvpncan3t 8853	Subtraction and addition of equal Hilbert space vectors..
|-