mmtheorems92 - 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 - 9101-9200 - Page 92 of 123

Type	Label	Description
Statement
Syntax	ck 9101	Extend class notation with the outer product of two vectors in Dirac bra-ket notation.
class ketbra
Syntax	cleo 9102	Extend class notation with positive operator ordering.
class <_op
Syntax	cei 9103	Extend class notation with Hilbert space eigenvector function.
class eigvec
Syntax	cel 9104	Extend class notation with Hilbert space eigenvalue function.
class eigval
Syntax	cspc 9105	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 9106	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 9107	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	cat 9108	Extend class notation with set of atoms on a Hilbert lattice.
class Atoms
Syntax	ccv 9109	Extend class notation with the covers relation on a Hilbert lattice.
class <o
Syntax	cmd 9110	Extend class notation with the modular pair relation on a Hilbert lattice.
class MH
Syntax	cdmd 9111	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class MH*
Preliminary ZFC lemmas
Definition	df-hnorm 9112	Define the function for the norm of a vector of Hilbert space. See normval 9266 for its value and normcl 9267 for its closure. Theorems norm-i.i 9276, norm-ii.i 9280, and norm-iii.i 9282 show it has the expected properties of a norm. In the literature, the norm of A is usually written "|| A ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in [Beran] p. 96.
|- normh = {<.x, y>. | (x e. dom dom .ih /\ y = (sqr` (x .ih x)))}
Definition	df-hba 9113	Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 9144). Note that H~ is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. This definition can be proved independently from those axioms as as theorem hhba 9310.
|- H~ = (BaseSet` <.<. +h , .h >., normh>.)
Definition	df-h0v 9114	Define the zero vector of Hilbert space. Note that 0v is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as theorem hh0v 9311.
|- 0h = (0v` <.<. +h , .h >., normh>.)
Definition	df-hvsub 9115	Define vector subtraction. See hvsubvali 9165 for its value and hvsubcli 9166 for its closure.
|- -h = {<.<.x, y>., z>. | ((x e. H~ /\ y e. H~) /\ z = (x +h (-u1 .h y)))}
Definition	df-hlim 9116	Define the limit relation for Hilbert space. See hlimi 9332 for its relational expression. Note that f:NN-->H~ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96.
|- ~~>v = {<.f, w>. | ((f:NN-->H~ /\ w e. H~) /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x)))}
Definition	df-hcau 9117	Define the set of Cauchy sequences on a Hilbert space. See hcau 9327 for its membership relation. Note that f:NN-->H~ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96.
|- Cauchy = {f | (f:NN-->H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)))}
Theorem	h2hva 9118	The group (addition) operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- +h = (+v` U)
Theorem	h2hsm 9119	The scalar product operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- .h = (.s` U)
Theorem	h2hnm 9120	The norm function of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- normh = (norm` U)
Theorem	h2hvs 9121	The vector subtraction operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (BaseSet` U)   =>   |- -h = (-v` U)
Theorem	h2hmetba 9122	The base set for the metric for Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (BaseSet` U)   &   |- D = (IndMet` U)   =>   |- H~ = dom dom D
Theorem	h2hmetdval 9123	Value of the distance function of the metric space of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (BaseSet` U)   &   |- D = (IndMet` U)   =>   |- ((A e. H~ /\ B e. H~) -> (ADB) = (normh` (A -h B)))
Theorem	h2hcau 9124	The Cauchy sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (BaseSet` U)   &   |- D = (IndMet` U)   =>   |- Cauchy = ((Cau` D) i^i (H~ ^m NN))
Theorem	h2hlm 9125	The limit sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (BaseSet` U)   &   |- D = (IndMet` U)   =>   |- ~~>v = ((~~>m` D) |` (H~ ^m NN))
Derive the Hilbert space axioms from ZFC set theory
Theorem	axhilex 9126	Derive axiom ax-hilex 9144 from Hilbert space under ZF set theory. Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of theorems axhilex 9126 through axhcompl 9143, using ZFC set theory only. These show that if we are given a known, fixed Hilbert space U = <.<. +h , .h >., normh>. that satisfies their hypotheses, then we can derive the Hilbert space axioms as theorems of ZFC set theory. In practice, in order to use these theorems to convert the Hilbert Space explorer to a ZFC-only subtheory, we would also have to provide definitions for the 3 (otherwise primitive) class constants +h, .h, and .ih before df-hnorm 9112 above. See also the comment in ax-hilex 9144.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- H~ e. V
Theorem	axhfvadd 9127	Derive axiom ax-hfvadd 9145 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- +h :(H~ X. H~)-->H~
Theorem	axhvcom 9128	Derive axiom ax-hvcom 9146 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))
Theorem	axhvass 9129	Derive axiom ax-hvass 9147 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) +h C) = (A +h (B +h C)))
Theorem	axhv0cl 9130	Derive axiom ax-hv0cl 9148 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- 0h e. H~
Theorem	axhvaddid 9131	Derive axiom ax-hvaddid 9149 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (A +h 0h) = A)
Theorem	axhfvmul 9132	Derive axiom ax-hfvmul 9150 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- .h :(CC X. H~)-->H~
Theorem	axhvmulid 9133	Derive axiom ax-hvmulid 9151 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (1 .h A) = A)
Theorem	axhvmulass 9134	Derive axiom ax-hvmulass 9152 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 9135	Derive axiom ax-hvdistr1 9153 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 9136	Derive axiom ax-hvdistr2 9154 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 9137	Derive axiom ax-hvmul0 9155 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (0 .h A) = 0h)
Theorem	axhfi 9138	Derive axiom ax-hfi 9222 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- .ih :(H~ X. H~)-->CC
Theorem	axhis1 9139	Derive axiom ax-his1 9225 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 9140	Derive axiom ax-his2 9226 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 9141	Derive axiom ax-his3 9227 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 9142	Derive axiom ax-his4 9228 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 9143	Derive axiom ax-hcompl 9347 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 9144	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 9144, ax-hfvadd 9145, ax-hvcom 9146, ax-hvass 9147, ax-hv0cl 9148, ax-hvaddid 9149, ax-hfvmul 9150, ax-hvmulid 9151, ax-hvmulass 9152, ax-hvdistr1 9153, ax-hvdistr2 9154, ax-hvmul0 9155, ax-hfi 9222, ax-his1 9225, ax-his2 9226, ax-his3 9227, ax-his4 9228, and ax-hcompl 9347. 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 9126, axhfvadd 9127, axhvcom 9128, axhvass 9129, axhv0cl 9130, axhvaddid 9131 , axhfvmul 9132, axhvmulid 9133, axhvmulass 9134, axhvdistr1 9135, axhvdistr2 9136 , axhvmul0 9137, axhfi 9138, axhis1 9139, axhis2 9140, axhis3 9141, axhis4 9142, and axhcompl 9143 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 9126.
|- H~ e. V
Axiom	ax-hfvadd 9145	Vector addition is an operation on H~.
|- +h :(H~ X. H~)-->H~
Axiom	ax-hvcom 9146	Vector addition is commutative.
|- ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))
Axiom	ax-hvass 9147	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 9148	The zero vector is in the vector space.
|- 0h e. H~
Axiom	ax-hvaddid 9149	Addition with the zero vector.
|- (A e. H~ -> (A +h 0h) = A)
Axiom	ax-hfvmul 9150	Scalar multiplication is an operation on CC and H~.
|- .h :(CC X. H~)-->H~
Axiom	ax-hvmulid 9151	Scalar multiplication by one.
|- (A e. H~ -> (1 .h A) = A)
Axiom	ax-hvmulass 9152	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 9153	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 9154	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 9155	Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 9170 and hvsubval 9161).
|- (A e. H~ -> (0 .h A) = 0h)
Vector operations
Theorem	hvmulex 9156	The Hilbert space scalar product operation is a set.
|- .h e. V
Theorem	hvaddcl 9157	Closure of vector addition.
|- ((A e. H~ /\ B e. H~) -> (A +h B) e. H~)
Theorem	hvmulcl 9158	Closure of scalar multiplication.
|- ((A e. CC /\ B e. H~) -> (A .h B) e. H~)
Theorem	hvmulcli 9159	Closure inference for scalar multiplication.
|- A e. CC   &   |- B e. H~   =>   |- (A .h B) e. H~
Theorem	hvsubopr 9160	Mapping domain and codomain of vector subtraction.
|- -h :(H~ X. H~)-->H~
Theorem	hvsubval 9161	Value of vector subtraction.
|- ((A e. H~ /\ B e. H~) -> (A -h B) = (A +h (-u1 .h B)))
Theorem	hvsubcl 9162	Closure of vector subtraction.
|- ((A e. H~ /\ B e. H~) -> (A -h B) e. H~)
Theorem	hvaddcli 9163	Closure of vector addition.
|- A e. H~   &   |- B e. H~   =>   |- (A +h B) e. H~
Theorem	hvcomi 9164	Commutation of vector addition.
|- A e. H~   &   |- B e. H~   =>   |- (A +h B) = (B +h A)
Theorem	hvsubvali 9165	Value of vector subtraction definition.
|- A e. H~   &   |- B e. H~   =>   |- (A -h B) = (A +h (-u1 .h B))
Theorem	hvsubcli 9166	Closure of vector subtraction.
|- A e. H~   &   |- B e. H~   =>   |- (A -h B) e. H~
Theorem	hvaddid2 9167	Addition with the zero vector.
|- (A e. H~ -> (0h +h A) = A)
Theorem	hvmul0 9168	Scalar multiplication with the zero vector.
|- (A e. CC -> (A .h 0h) = 0h)
Theorem	hvmul0or 9169	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 9170	Subtraction of a vector from itself.
|- (A e. H~ -> (A -h A) = 0h)
Theorem	hvnegid 9171	Addition of negative of a vector to itself.
|- (A e. H~ -> (A +h (-u1 .h A)) = 0h)
Theorem	hv2neg 9172	Two ways to express the negative of a vector.
|- (A e. H~ -> (0h -h A) = (-u1 .h A))
Theorem	hvaddid2i 9173	Addition with the zero vector.
|- A e. H~   =>   |- (0h +h A) = A
Theorem	hvnegidi 9174	Addition of negative of a vector to itself.
|- A e. H~   =>   |- (A +h (-u1 .h A)) = 0h
Theorem	hv2negi 9175	Two ways to express the negative of a vector.
|- A e. H~   =>   |- (0h -h A) = (-u1 .h A)
Theorem	hvm1neg 9176	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 9177	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 9178	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) +h C) = ((A +h C) +h B))
Theorem	hvadd12 9179	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A +h (B +h C)) = (B +h (A +h C)))
Theorem	hvadd4 9180	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 9181	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 9182	Commutative/associative law.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A +h (B -h C)) = (B +h (A -h C)))
Theorem	hvpncan 9183	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. H~ /\ B e. H~) -> ((A +h B) -h B) = A)
Theorem	hvpncan2 9184	Addition/subtraction cancellation law for vectors in Hilbert space.
|- ((A e. H~ /\ B e. H~) -> ((A +h B) -h A) = B)
Theorem	hvaddsubass 9185	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 9186	Subtraction and addition of equal Hilbert space vectors..
|- ((A e. H~ /\ B e. H~) -> (A +h (B -h A)) = B)
Theorem	hvmulcom 9187	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 9188	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 9189	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 9190	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 9191	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 9192	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 9193	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 9194	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 9195	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 9196	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 9197	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 9198	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 9199	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 9200	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))