mmtheorems106 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 10501-10600 - Page 106 of 175

Type	Label	Description
Statement
Introduce the vector space axioms for a Hilbert space
Axiom	ax-hilex 10501	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 10501, ax-hfvadd 10502, ax-hvcom 10503, ax-hvass 10504, ax-hv0cl 10505, ax-hvaddid 10506, ax-hfvmul 10507, ax-hvmulid 10508, ax-hvmulass 10509, ax-hvdistr1 10510, ax-hvdistr2 10511, ax-hvmul0 10512, ax-hfi 10579, ax-his1 10582, ax-his2 10583, ax-his3 10584, ax-his4 10585, and ax-hcompl 10704. The axioms specify the properties of 5 primitive symbols, ~H, +h, .h, 0h, and .ih. If we 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 10483, axhfvadd 10484, axhvcom 10485, axhvass 10486, axhv0cl 10487, axhvaddid 10488, axhfvmul 10489, axhvmulid 10490, axhvmulass 10491, axhvdistr1 10492, axhvdistr2 10493, axhvmul0 10494, axhfi 10495, axhis1 10496, axhis2 10497, axhis3 10498, axhis4 10499, and axhcompl 10500 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 10483.
|- ~H e. _V
Axiom	ax-hfvadd 10502	Vector addition is an operation on ~H.
|- +h :(~H X. ~H)-->~H
Axiom	ax-hvcom 10503	Vector addition is commutative.
|- ((A e. ~H /\ B e. ~H) -> (A +h B) = (B +h A))
Axiom	ax-hvass 10504	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 10505	The zero vector is in the vector space.
|- 0h e. ~H
Axiom	ax-hvaddid 10506	Addition with the zero vector.
|- (A e. ~H -> (A +h 0h) = A)
Axiom	ax-hfvmul 10507	Scalar multiplication is an operation on CC and ~H.
|- .h :(CC X. ~H)-->~H
Axiom	ax-hvmulid 10508	Scalar multiplication by one.
|- (A e. ~H -> (1 .h A) = A)
Axiom	ax-hvmulass 10509	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 10510	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 10511	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 10512	Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 10527 and hvsubval 10518).
|- (A e. ~H -> (0 .h A) = 0h)
Vector operations
Theorem	hvmulex 10513	The Hilbert space scalar product operation is a set.
|- .h e. _V
Theorem	hvaddcl 10514	Closure of vector addition.
|- ((A e. ~H /\ B e. ~H) -> (A +h B) e. ~H)
Theorem	hvmulcl 10515	Closure of scalar multiplication.
|- ((A e. CC /\ B e. ~H) -> (A .h B) e. ~H)
Theorem	hvmulcli 10516	Closure inference for scalar multiplication.
|- A e. CC   &   |- B e. ~H   =>   |- (A .h B) e. ~H
Theorem	hvsubopr 10517	Mapping domain and codomain of vector subtraction.
|- -h :(~H X. ~H)-->~H
Theorem	hvsubval 10518	Value of vector subtraction.
|- ((A e. ~H /\ B e. ~H) -> (A -h B) = (A +h (-u1 .h B)))
Theorem	hvsubcl 10519	Closure of vector subtraction.
|- ((A e. ~H /\ B e. ~H) -> (A -h B) e. ~H)
Theorem	hvaddcli 10520	Closure of vector addition.
|- A e. ~H   &   |- B e. ~H   =>   |- (A +h B) e. ~H
Theorem	hvcomi 10521	Commutation of vector addition.
|- A e. ~H   &   |- B e. ~H   =>   |- (A +h B) = (B +h A)
Theorem	hvsubvali 10522	Value of vector subtraction definition.
|- A e. ~H   &   |- B e. ~H   =>   |- (A -h B) = (A +h (-u1 .h B))
Theorem	hvsubcli 10523	Closure of vector subtraction.
|- A e. ~H   &   |- B e. ~H   =>   |- (A -h B) e. ~H
Theorem	hvaddid2 10524	Addition with the zero vector.
|- (A e. ~H -> (0h +h A) = A)
Theorem	hvmul0 10525	Scalar multiplication with the zero vector.
|- (A e. CC -> (A .h 0h) = 0h)
Theorem	hvmul0or 10526	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	hvsubid 10527	Subtraction of a vector from itself.
|- (A e. ~H -> (A -h A) = 0h)
Theorem	hvnegid 10528	Addition of negative of a vector to itself.
|- (A e. ~H -> (A +h (-u1 .h A)) = 0h)
Theorem	hv2neg 10529	Two ways to express the negative of a vector.
|- (A e. ~H -> (0h -h A) = (-u1 .h A))
Theorem	hvaddid2i 10530	Addition with the zero vector.
|- A e. ~H   =>   |- (0h +h A) = A
Theorem	hvnegidi 10531	Addition of negative of a vector to itself.
|- A e. ~H   =>   |- (A +h (-u1 .h A)) = 0h
Theorem	hv2negi 10532	Two ways to express the negative of a vector.
|- A e. ~H   =>   |- (0h -h A) = (-u1 .h A)
Theorem	hvm1neg 10533	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	hvaddsubval 10534	Value of vector addition in terms of vector subtraction.
|- ((A e. ~H /\ B e. ~H) -> (A +h B) = (A -h (-u1 .h B)))
Theorem	hvadd23 10535	Commutative/associative law.
|- ((A e. ~H /\ B e. ~H /\ C e. ~H) -> ((A +h B) +h C) = ((A +h C) +h B))
Theorem	hvadd12 10536	Commutative/associative law.
|- ((A e. ~H /\ B e. ~H /\ C e. ~H) -> (A +h (B +h C)) = (B +h (A +h C)))
Theorem	hvadd4 10537	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	hvsub4 10538	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	hvaddsub12 10539	Commutative/associative law.
|- ((A e. ~H /\ B e. ~H /\ C e. ~H) -> (A +h (B -h C)) = (B +h (A -h C)))
Theorem	hvpncan 10540	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. ~H /\ B e. ~H) -> ((A +h B) -h B) = A)
Theorem	hvpncan2 10541	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. ~H /\ B e. ~H) -> ((A +h B) -h A) = B)
Theorem	hvaddsubass 10542	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	hvpncan3 10543	Subtraction and addition of equal Hilbert space vectors..
|- ((A e. ~H /\ B e. ~H) -> (A +h (B -h A)) = B)
Theorem	hvmulcom 10544	Scalar multiplication commutative law.
|- ((A e. CC /\ B e. CC /\ C e. ~H) -> (A .h (B .h C)) = (B .h (A .h C)))
Theorem	hvmulassi 10545	Scalar multiplication associative law.
|- A e. CC   &   |- B e. CC   &   |- C e. ~H   =>   |- ((A x. B) .h C) = (A .h (B .h C))
Theorem	hvmulcomi 10546	Scalar multiplication commutative law.
|- A e. CC   &   |- B e. CC   &   |- C e. ~H   =>   |- (A .h (B .h C)) = (B .h (A .h C))
Theorem	hvmul2negi 10547	Double negative in scalar multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. ~H   =>   |- (-uA .h (-uB .h C)) = (A .h (B .h C))
Theorem	hvsubdistr1 10548	Scalar multiplication distributive law for subtraction.
|- ((A e. CC /\ B e. ~H /\ C e. ~H) -> (A .h (B -h C)) = ((A .h B) -h (A .h C)))
Theorem	hvsubdistr2 10549	Scalar multiplication distributive law for subtraction.
|- ((A e. CC /\ B e. CC /\ C e. ~H) -> ((A - B) .h C) = ((A .h C) -h (B .h C)))
Theorem	hvdistr1i 10550	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))
Theorem	hvsubdistr1i 10551	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))
Theorem	hvassi 10552	Hilbert vector space associative law.
|- A e. ~H   &   |- B e. ~H   &   |- C e. ~H   =>   |- ((A +h B) +h C) = (A +h (B +h C))
Theorem	hvadd23i 10553	Hilbert vector space commutative/associative law.
|- A e. ~H   &   |- B e. ~H   &   |- C e. ~H   =>   |- ((A +h B) +h C) = ((A +h C) +h B)
Theorem	hvsubassi 10554	Hilbert vector space associative law for subtraction.
|- A e. ~H   &   |- B e. ~H   &   |- C e. ~H   =>   |- ((A -h B) -h C) = (A -h (B +h C))
Theorem	hvsub23i 10555	Hilbert vector space commutative/associative law.
|- A e. ~H   &   |- B e. ~H   &   |- C e. ~H   =>   |- ((A -h B) -h C) = ((A -h C) -h B)
Theorem	hvadd12i 10556	Hilbert vector space commutative/associative law.
|- A e. ~H   &   |- B e. ~H   &   |- C e. ~H   =>   |- (A +h (B +h C)) = (B +h (A +h C))
Theorem	hvadd4i 10557	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	hvsubsub4i 10558	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 10559	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 10560	Two times a vector.
|- (A e. ~H -> (2 .h A) = (A +h A))
Theorem	hvnegdii 10561	Distribution of negative over subtraction.
|- A e. ~H   &   |- B e. ~H   =>   |- (-u1 .h (A -h B)) = (B -h A)
Theorem	hvsubeq0i 10562	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 10563	Vector cancellation law.
|- A e. ~H   &   |- B e. ~H   =>   |- ((A +h B) +h (A -h B)) = (2 .h A)
Theorem	hvaddcani 10564	Cancellation law for vector addition.
|- A e. ~H   &   |- B e. ~H   &   |- C e. ~H   =>   |- ((A +h B) = (A +h C) <-> B = C)
Theorem	hvsubaddi 10565	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 10566	Distribution of negative over subtraction.
|- ((A e. ~H /\ B e. ~H) -> (-u1 .h (A -h B)) = (B -h A))
Theorem	hvsubeq0 10567	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 10568	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 10569	Cancellation law for vector addition.
|- ((A e. ~H /\ B e. ~H /\ C e. ~H) -> ((A +h B) = (A +h C) <-> B = C))
Theorem	hvaddcan2 10570	Cancellation law for vector addition.
|- ((A e. ~H /\ B e. ~H /\ C e. ~H) -> ((A +h C) = (B +h C) <-> A = B))
Theorem	hvmulcan 10571	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 10572	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 10573	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 10574	Cancellation law for vector addition.
|- ((A e. ~H /\ B e. ~H /\ C e. ~H) -> ((A -h B) = (A -h C) <-> B = C))
Theorem	hvsubcan2 10575	Cancellation law for vector addition.
|- ((A e. ~H /\ B e. ~H /\ C e. ~H) -> ((A -h C) = (B -h C) <-> A = B))
Theorem	hvsub0 10576	Subtraction of a zero vector.
|- (A e. ~H -> (A -h 0h) = A)
Theorem	hvsubadd 10577	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 10578	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 10579	Inner product maps pairs from ~H to CC.
|- .ih :(~H X. ~H)-->CC
Theorem	hicl 10580	Closure of inner product.
|- ((A e. ~H /\ B e. ~H) -> (A .ih B) e. CC)
Theorem	hicli 10581	Closure inference for inner product.
|- A e. ~H   &   |- B e. ~H   =>   |- (A .ih B) e. CC
Axiom	ax-his1 10582	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that *` x is the complex conjugate cjval 8013 of x. In the literature, the inner product of A and B is usually written <.A, B>., but our operation notation co 4884 allows us to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 3053. Physicists use <.B | A>., called Dirac bra-ket notation, to represent this operation; see comments in df-bra 11413.
|- ((A e. ~H /\ B e. ~H) -> (A .ih B) = (*` (B .ih A)))
Axiom	ax-his2 10583	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 10584	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 11413 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 10585	Identity law for inner product. Postulate (S4) of [Beran] p. 95.
|- ((A e. ~H /\ A =/= 0h) -> 0 < (A .ih A))
Inner product
Theorem	his5 10586	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 10587	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 10588	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 10589	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 10590	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 10591	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 10592	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 10593	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 10594	Real closure of inner product with self.
|- (A e. ~H -> (A .ih A) e. RR)
Theorem	hi01 10595	Inner product with the 0 vector.
|- (A e. ~H -> (0h .ih A) = 0)
Theorem	hi02 10596	Inner product with the 0 vector.
|- (A e. ~H -> (A .ih 0h) = 0)
Theorem	hiidge0 10597	Inner product with self is not negative.
|- (A e. ~H -> 0 <_ (A .ih A))
Theorem	his6 10598	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 10599	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 10600	Commuted inner products have the same absolute values.
|- ((A e. ~H /\ B e. ~H) -> (abs` (A .ih B)) = (abs` (B .ih A)))