mmtheorems91 - 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-10688

Statement List for Metamath Proof Explorer - 9001-9100 - Page 91 of 107

Type	Label	Description
Statement
Theorem	hilid 9001	The group identity element of Hilbert space vector addition is the zero vector.
|- (Id` +h ) = 0h
Theorem	hilvc 9002	Hilbert space is a complex vector space. Vector addition is +h, and scalar product is .h.
|- <. +h , .h >. e. CVec
Theorem	hilnorm 9003	Hilbert space norm in terms of vector space norm.
|- H~ = (Base` U)   &   |- .ih = (.i` U)   &   |- U e. NrmCVec   =>   |- normh = (norm` U)
Theorem	hilhh 9004	Deduce the structure of Hilbert space from its components.
|- H~ = (Base` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- U e. NrmCVec   =>   |- U = <.<. +h , .h >., normh>.
Theorem	hhnv 9005	Hilbert space is a normed complex vector space.
|- U = <.<. +h , .h >., normh>.   =>   |- U e. NrmCVec
Theorem	hhva 9006	The group (addition) operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- +h = (+v` U)
Theorem	hhba 9007	The base set of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- H~ = (Base` U)
Theorem	hh0v 9008	The zero vector of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- 0h = (0v` U)
Theorem	hhsm 9009	The scalar product operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- .h = (.s` U)
Theorem	hhvs 9010	The vector subtraction operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- -h = (-v` U)
Theorem	hhnm 9011	The norm function of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- normh = (norm` U)
Theorem	hhims 9012	The induced metric of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (normh o. -h )   =>   |- D = (IndMet` U)
Theorem	hhims2 9013	Hilbert space distance metric.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- D = (normh o. -h )
Theorem	hhmet 9014	The induced metric of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- D e. Met
Theorem	hhmetba 9015	The base set for the metric for Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- H~ = dom dom D
Theorem	hhmetdval 9016	Value of the distance function of the metric space of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- ((A e. H~ /\ B e. H~) -> (ADB) = (normh` (A -h B)))
Theorem	hhip 9017	The inner product operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- .ih = (.i` U)
Theorem	hhph 9018	The Hilbert space of the Hilbert Space Explorer is an inner product space.
|- U = <.<. +h , .h >., normh>.   =>   |- U e. CPreHil
Bunjakovaskij-Cauchy-Schwarz inequality
Theorem	bcsALT 9019	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98.
|- A e. H~   &   |- B e. H~   =>   |- (abs` (A .ih B)) <_ ((normh` A) x. (normh` B))
Theorem	bcsHIL 9020	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Proved from ZFC version.)
|- A e. H~   &   |- B e. H~   =>   |- (abs` (A .ih B)) <_ ((normh` A) x. (normh` B))
Theorem	bcst 9021	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98.
|- ((A e. H~ /\ B e. H~) -> (abs` (A .ih B)) <_ ((normh` A) x. (normh` B)))
Theorem	bcs2t 9022	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsHIL 9020.
|- ((A e. H~ /\ B e. H~ /\ (normh` A) <_ 1) -> (abs` (A .ih B)) <_ (normh` B))
Theorem	bcs3t 9023	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsHIL 9020.
|- ((A e. H~ /\ B e. H~ /\ (normh` B) <_ 1) -> (abs` (A .ih B)) <_ (normh` A))
Cauchy sequences and limits
Theorem	hcau 9024	Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in [Beran] p. 96.
|- (F e. Cauchy <-> (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	hcauseq 9025	A Cauchy sequences on a Hilbert space is a sequence.
|- (F e. Cauchy -> F:NN-->H~)
Theorem	hcaucvg 9026	A Cauchy sequence on a Hilbert space converges.
|- (F e. Cauchy -> 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	seq1hcau 9027	A sequence on a Hilbert space is a Cauchy sequence if it converges.
|- (F:NN-->H~ -> (F e. Cauchy <-> 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	hcau2 9028	Alternate representation of a Hilbert space Cauchy sequence.
|- (F e. Cauchy <-> (F:NN-->H~ /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((F` k) -h (F` j))) < x))))
Theorem	hlim 9029	Express the predicate: The limit of vector sequence F in a Hilbert space is A, i.e. F converges to A. This means that for any real x, no matter how small, there always exists an integer y such that the norm of any later vector in the sequence minus the limit is less than x. Definition of converge in [Beran] p. 96.
|- F e. V   &   |- A e. V   =>   |- (F ~~>v A <-> ((F:NN-->H~ /\ A e. H~) /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < x))))
Theorem	hlimseq 9030	A sequence with a limit on a Hilbert space is a sequence.
|- F e. V   &   |- A e. V   =>   |- (F ~~>v A -> F:NN-->H~)
Theorem	hlimvec 9031	Closure of the limit of a sequence on Hilbert space.
|- F e. V   &   |- A e. V   =>   |- (F ~~>v A -> A e. H~)
Theorem	hlimconv 9032	Convergence of a sequence on a Hilbert space.
|- F e. V   &   |- A e. V   =>   |- (F ~~>v A -> A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < x)))
Theorem	hlim2 9033	The limit of a sequence on a Hilbert space.
|- ((F:NN-->H~ /\ A e. H~) -> (F ~~>v A <-> A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < x))))
Derivation of the completeness axiom from ZF set theory
Theorem	hilmet 9034	The Hilbert space norm determines a metric space.
|- D = (normh o. -h )   =>   |- D e. Met
Theorem	hilmetdval 9035	Value of the distance function of the metric space of Hilbert space.
|- D = (normh o. -h )   =>   |- ((A e. H~ /\ B e. H~) -> (ADB) = (normh` (A -h B)))
Theorem	hilmetba 9036	The base set for the metric for Hilbert space.
|- D = (normh o. -h )   =>   |- H~ = dom dom D
Theorem	hilims 9037	Hilbert space distance metric.
|- H~ = (Base` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- D = (IndMet` U)   &   |- U e. NrmCVec   =>   |- D = (normh o. -h )
Theorem	hillim 9038	Hilbert space limit in terms of metric space limit.
|- H~ = (Base` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- D = (IndMet` U)   &   |- U e. NrmCVec   =>   |- ~~>v = ((~~>m` D) |` (H~ ^m NN))
Theorem	hilcau 9039	Hilbert space Cauchy sequences in terms of metric space Cauchy sequences.
|- H~ = (Base` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- D = (IndMet` U)   &   |- U e. NrmCVec   =>   |- Cauchy = ((Cau` D) i^i (H~ ^m NN))
Theorem	hhlm 9040	The limit sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- ~~>v = ((~~>m` D) |` (H~ ^m NN))
Theorem	hhcau 9041	The Cauchy sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- Cauchy = ((Cau` D) i^i (H~ ^m NN))
Theorem	hhcmpl 9042	Lemma used for derivation of the completeness axiom ax-hcompl 9044 from ZFC Hilbert space theory.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   &   |- (F e. (Cau` D) -> E.x e. H~ F(~~>m` D)x)   =>   |- (F e. Cauchy -> E.x e. H~ F ~~>v x)
Theorem	hilcompl 9043	Lemma used for derivation of the completeness axiom ax-hcompl 9044 from ZFC Hilbert space theory. The first 5 hypotheses would be satisfied by the definitions described in ax-hilex 8842; the 6th would be satisfied by eqid 1473; the 7th by a given fixed Hilbert space; and the last by theorem hlcompl 8575.
|- H~ = (Base` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- D = (IndMet` U)   &   |- U e. CHil   &   |- (F e. (Cau` D) -> E.x e. H~ F(~~>m` D)x)   =>   |- (F e. Cauchy -> E.x e. H~ F ~~>v x)
Completeness postulate for a Hilbert space
Axiom