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-10700 108 10701-10722

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

Type	Label	Description
Statement
Syntax	chod 8801	Extend class notation with difference of Hilbert space operators.
class -op
Syntax	chfs 8802	Extend class notation with sum of Hilbert space functionals.
class +fn
Syntax	chft 8803	Extend class notation with scalar product of Hilbert space functional.
class .fn
Syntax	ch0o 8804	Extend class notation with the Hilbert space zero operator.
class 0hop
Syntax	chio 8805	Extend class notation with Hilbert space identity operator.
class Iop
Syntax	cnop 8806	Extend class notation with the operator norm function.
class normop
Syntax	cco 8807	Extend class notation with set of continuous Hilbert space operators.
class ConOp
Syntax	clo 8808	Extend class notation with set of linear Hilbert space operators.
class LinOp
Syntax	cbo 8809	Extend class notation with set of bounded linear operators.
class BndLinOp
Syntax	cuo 8810	Extend class notation with set of unitary Hilbert space operators.
class UniOp
Syntax	cho 8811	Extend class notation with set of Hermitian Hilbert space operators.
class HrmOp
Syntax	cnmf 8812	Extend class notation with the functional norm function.
class normfn
Syntax	cnl 8813	Extend class notation with the functional nullspace function.
class null
Syntax	ccnf 8814	Extend class notation with set of continuous Hilbert space functionals.
class ConFn
Syntax	clf 8815	Extend class notation with set of linear Hilbert space functionals.
class LinFn
Syntax	cado 8816	Extend class notation with Hilbert space adjoint function.
class adjh
Syntax	cbr 8817	Extend class notation with the bra of a vector in Dirac bra-ket notation.
class bra
Syntax	ck 8818	Extend class notation with the outer product of two vectors in Dirac bra-ket notation.
class ketbra
Syntax	cleo 8819	Extend class notation with positive operator ordering.
class <_op
Syntax	cei 8820	Extend class notation with Hilbert space eigenvector function.
class eigvec
Syntax	cel 8821	Extend class notation with Hilbert space eigenvalue function.
class eigval
Syntax	cspc 8822	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 8823	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 8824	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	cat 8825	Extend class notation with set of atoms on a Hilbert lattice.
class Atoms
Syntax	ccv 8826	Extend class notation with the covers relation on a Hilbert lattice.
class <o
Syntax	cmd 8827	Extend class notation with the modular pair relation on a Hilbert lattice.
class MH
Syntax	cdmd 8828	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class MH*
Preliminary ZFC lemmas
Definition	df-hnorm 8829	Define the function for the norm of a vector of Hilbert space. See normvalt 8982 for its value and normclt 8983 for its closure. Theorems norm-i 8992, norm-ii 8996, and norm-iii 8998 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 8830	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 9026.
|- H~ = (Base` <.<. +h , .h >., normh>.)
Definition	df-h0v 8831	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 9027.
|- 0h = (0v` <.<. +h , .h >., normh>.)
Definition	df-hvsub 8832	Define vector subtraction. See hvsubval 8882 for its value and hvsubcl 8883 for its closure.
|- -h = {<.<.x, y>., z>. | ((x e. H~ /\ y e. H~) /\ z = (x +h (-u1 .h y)))}
Definition	df-hlim 8833	Define the limit relation for Hilbert space. See hlim 9048 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 8834	Define the set of Cauchy sequences on a Hilbert space. See hcau 9043 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 8835	The group (addition) operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- +h = (+v` U)
Theorem	h2hsm 8836	The scalar product operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- .h = (.s` U)
Theorem	h2hnm 8837	The norm function of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   =>   |- normh = (norm` U)
Theorem	h2hvs 8838	The vector subtraction operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- U e. NrmCVec   &   |- H~ = (Base` U)   =>   |- -h = (-v` U)
Theorem	h2hmetba 8839	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 8840	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 8841	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 8842	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 8843	Derive axiom ax-hilex 8861 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 8843 through axhcompl 8860, 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 8829 above. See also the comment in ax-hilex 8861.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- H~ e. V
Theorem	axhfvadd 8844	Derive axiom ax-hfvadd 8862 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- +h :(H~ X. H~)-->H~
Theorem	axhvcom 8845	Derive axiom ax-hvcom 8863 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 8846	Derive axiom ax-hvass 8864 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 8847	Derive axiom ax-hv0cl 8865 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- 0h e. H~
Theorem	axhvaddid 8848	Derive axiom ax-hvaddid 8866 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (A +h 0h) = A)
Theorem	axhfvmul 8849	Derive axiom ax-hfvmul 8867 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- .h :(CC X. H~)-->H~
Theorem	axhvmulid 8850	Derive axiom ax-hvmulid 8868 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (1 .h A) = A)
Theorem	axhvmulass 8851	Derive axiom ax-hvmulass 8869 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 8852	Derive axiom ax-hvdistr1 8870 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 8853	Derive axiom ax-hvdistr2 8871 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 8854	Derive axiom ax-hvmul0 8872 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (A e. H~ -> (0 .h A) = 0h)
Theorem	axhfi 8855	Derive axiom ax-hfi 8938 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- .ih :(H~ X. H~)-->CC
Theorem	axhis1 8856	Derive axiom ax-his1 8941 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 8857	Derive axiom ax-his2 8942 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 8858	Derive axiom ax-his3 8943 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 8859	Derive axiom ax-his4 8944 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 8860	Derive axiom ax-hcompl 9063 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 8861	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 8861, ax-hfvadd 8862, ax-hvcom 8863, ax-hvass 8864, ax-hv0cl 8865, ax-hvaddid 8866, ax-hfvmul