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-10683

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

Type	Label	Description
Statement
Syntax	cspc 8801	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 8802	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 8803	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	cat 8804	Extend class notation with set of atoms on a Hilbert lattice.
class Atoms
Syntax	ccv 8805	Extend class notation with the covers relation on a Hilbert lattice.
class <o
Syntax	cmd 8806	Extend class notation with the modular pair relation on a Hilbert lattice.
class MH
Syntax	cdmd 8807	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class MH*
Preliminary ZFC lemmas
Definition	df-hnorm 8808	Define the function for the norm of a vector of Hilbert space. See normvalt 8961 for its value and normclt 8962 for its closure. Theorems norm-i 8971, norm-ii 8975, and norm-iii 8977 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 8809	Define base set of Hilbert space. Note that H~ 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 hhba 9005.
|- H~ = (Base` <.<. +h , .h >., normh>.)
Definition	df-h0v 8810	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 9006.
|- 0h = (0v` <.<. +h , .h >., normh>.)
Definition	df-hvsub 8811	Define vector subtraction. See hvsubval 8861 for its value and hvsubcl 8862 for its closure.
|- -h = {<.<.x, y>., z>. | ((x e. H~ /\ y e. H~) /\ z = (x +h (-u1 .h y)))}
Definition	df-hlim 8812	Define the limit relation for Hilbert space. See hlim 9027 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 8813	Define the set of Cauchy sequences on a Hilbert space. See hcau 9022 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 8814	The group (addition) operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- +h = (+v` U)
Theorem	h2hsm 8815	The scalar product operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- .h = (.s` U)
Theorem	h2hnm 8816	The norm function of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- normh = (norm` U)
Theorem	h2hvs 8817	The vector subtraction operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (Base` U)   =>   |- -h = (-v` U)
Theorem	h2hmetba 8818	The base set for the metric for Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (Base` U)   &   |- D = (IndMet` U)   =>   |- H~ = dom dom D
Theorem	h2hmetdval 8819	Value of the distance function of the metric space of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (Base` U)   &   |- D = (IndMet` U)   =>   |- ((A e. H~ /\ B e. H~) -> (ADB) = (normh` (A -h B)))
Theorem	h2hcau 8820	The Cauchy sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (Base` U)   &   |- D = (IndMet` U)   =>   |- Cauchy = ((Cau` D) i^i (H~ ^m NN))
Theorem	h2hlm 8821	The limit sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (Base` U)   &   |- D = (IndMet` U)   =>   |- ~~>v = ((~~>m` D) |` (H~ ^m NN))
Derive the Hilbert space axioms from ZFC set theory
Theorem	axhilex 8822	Derive axiom ax-hilex 8840 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 8822 through axhcompl 8839, 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 8808 above. See also the comment in ax-hilex 8840.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- H~ e. V
Theorem	axhfvadd 8823	Derive axiom ax-hfvadd 8841 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- +h :(H~ X. H~)-->H~
Theorem	axhvcom 8824	Derive axiom ax-hvcom 8842 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 8825	Derive axiom ax-hvass 8843 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 8826	Derive axiom ax-hv0cl 8844 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- 0h e. H~
Theorem	axhvaddid 8827	Derive axiom ax-hvaddid 8845 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (A +h 0h) = A)
Theorem	axhfvmul 8828	Derive axiom ax-hfvmul 8846 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- .h :(CC X. H~)-->H~
Theorem	axhvmulid 8829	Derive axiom ax-hvmulid 8847 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (1 .h A) = A)
Theorem	axhvmulass 8830	Derive axiom ax-hvmulass 8848 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 8831	Derive axiom ax-hvdistr1 8849 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 8832	Derive axiom ax-hvdistr2 8850 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 8833	Derive axiom ax-hvmul0 8851 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (0 .h A) = 0h)
Theorem	axhfi 8834	Derive axiom ax-hfi 8917 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- .ih :(H~ X. H~)-->CC
Theorem	axhis1 8835	Derive axiom ax-his1 8920 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 8836	Derive axiom ax-his2 8921 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 8837	Derive axiom ax-his3 8922 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 8838	Derive axiom ax-his4 8923 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 8839	Derive axiom ax-hcompl 9042 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 8840	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 8840, ax-hfvadd 8841, ax-hvcom 8842, ax-hvass 8843, ax-hv0cl 8844, ax-hvaddid 8845, ax-hfvmul 8846, ax-hvmulid 8847, ax-hvmulass 8848, ax-hvdistr1 8849, ax-hvdistr2 8850, ax-hvmul0 8851, ax-hfi 8917, ax-his1 8920, ax-his2 8921, ax-his3 8922, ax-his4 8923, and ax-hcompl 9042. 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 8822, axhfvadd 8823, axhvcom 8824, axhvass 8825, axhv0cl 8826, axhvaddid 8827 , axhfvmul 8828, axhvmulid 8829, axhvmulass 8830, axhvdistr1 8831, axhvdistr2 8832 , axhvmul0 8833, axhfi 8834, axhis1 8835, axhis2 8836, axhis3 8837, axhis4 8838, and axhcompl 8839 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 8822.
|- H~ e. V
Axiom	ax-hfvadd 8841	Vector addition is an operation on H~.
|- +h :(H~ X. H~)-->H~
Axiom	ax-hvcom 8842	Vector addition is commutative.
|- ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))
Axiom	ax-hvass 8843	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 8844	The zero vector is in the vector space.
|- 0h e. H~
Axiom	ax-hvaddid 8845	Addition with the zero vector.