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

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

Type	Label	Description
Statement
Theorem	bcsHIL 9001	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 9002	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 9003	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsHIL 9001.
|- ((A e. H~ /\ B e. H~ /\ (normh` A) <_ 1) -> (abs` (A .ih B)) <_ (normh` B))
Theorem	bcs3t 9004	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsHIL 9001.
|- ((A e. H~ /\ B e. H~ /\ (normh` B) <_ 1) -> (abs` (A .ih B)) <_ (normh` A))
Cauchy sequences and limits
Theorem	hcau 9005	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 9006	A Cauchy sequences on a Hilbert space is a sequence.
|- (F e. Cauchy -> F:NN-->H~)
Theorem	hcaucvg 9007	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 9008	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 9009	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 9010	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 9011	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 9012	Closure of the limit of a sequence on Hilbert space.
|- F e. V   &   |- A e. V   =>   |- (F ~~>v A -> A e. H~)
Theorem	hlimconv 9013	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 9014	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 9015	The Hilbert space norm determines a metric space.
|- D = (normh o. -h )   =>   |- D e. Met
Theorem	hilmetdval 9016	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 9017	The base set for the metric for Hilbert space.
|- D = (normh o. -h )   =>   |- H~ = dom dom D
Theorem	hilims 9018	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 9019	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 9020	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 9021	The limit sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- ~~>v = ((~~>m` D) |` (H~ ^m NN))
Theorem	hhcau 9022	The Cauchy sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- Cauchy = ((Cau` D) i^i (H~ ^m NN))
Theorem	hhcmpl 9023	Lemma used for derivation of the completeness axiom ax-hcompl 9025 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 9024	Lemma used for derivation of the completeness axiom ax-hcompl 9025 from ZFC Hilbert space theory. The first 5 hypotheses would be satisfied by the definitions described in ax-hilex 8823; the 6th would be satisfied by eqid 1474; the 7th by a given fixed Hilbert space; and the last by theorem hlcompl 8574.
|- 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	ax-hcompl 9025	Completeness of a Hilbert space.
|- (F e. Cauchy -> E.x e. H~ F ~~>v x)
Relate Hilbert space to ZFC pre-Hilbert and Hilbert spaces
Theorem	hhcms 9026	The Hilbert space induced metric determines a complete metric space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- D e. CMet
Theorem	hhhl 9027	The Hilbert space structure is a complex Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- U e. CHil
Theorem	hilcms 9028	The Hilbert space norm determines a complete metric space.
|- D = (normh o. -h )   =>   |- D e. CMet
Theorem	hilhl 9029	The Hilbert space of the Hilbert Space Explorer is a complex Hilbert space. (Contributed by Steve Rodriguez, 29-Apr-2007.)
|- <.<. +h , .h >., normh>. e. CHil
Subspaces
Definition	df-sh 9030	Define the set of subspaces of a Hilbert space. See sh 9032 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95.
|- SH = {h | ((h (_ H~ /\ 0h e. h) /\ (A.x e. h A.y e. h (x +h y) e. h /\ A.x e. CC A.y e. h (x .h y) e. h))}
Theorem	shex 9031	The set of subspaces of a Hilbert space exists (is a set).
|- SH e. V
Theorem	sh 9032	Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95.
|- (H e. SH <-> ((H (_ H~ /\ 0h e. H) /\ (A.x e. H A.y e. H (x +h y) e. H /\ A.x e. CC A.y e. H (x .h y) e. H)))
Theorem	shss 9033	A subspace is a subset of Hilbert space.
|- (H e. SH -> H (_ H~)
Theorem	shelt 9034	A member of a subspace of a Hilbert space is a vector.
|- ((H e. SH /\ A e. H) -> A e. H~)
Theorem	shssi 9035	A closed subspace of a Hilbert space is a subset of Hilbert space.
|- H e. SH   =>   |- H (_ H~
Theorem	shel 9036	A member of a subspace of a Hilbert space is a vector.
|- H e. SH   =>   |- (A e. H -> A e. H~)
Theorem	sheli 9037	A member of a subspace of a Hilbert space is a vector.
|- H e. SH   &   |- A e. H   =>   |- A e. H~
Theorem	sh0 9038	The zero vector belongs to any subspace of a Hilbert space.
|- (H e. SH -> 0h e. H)
Theorem	shaddclt 9039	Closure of vector addition in a subspace of a Hilbert space.
|- ((H e. SH /\ A e. H /\ B e. H) -> (A +h B) e. H)
Theorem	shaddcltOLD 9040	Closure of vector addition in a subspace of a Hilbert space.
|- (H e. SH -> ((A e. H /\ B e. H) -> (A +h B) e. H))
Theorem	shmulclt 9041	Closure of vector scalar multiplication in a subspace of a Hilbert space.
|- ((H e. SH /\ A e. CC /\ B e. H) -> (A .h B) e. H)
Theorem	shmulcltOLD 9042	Closure of vector scalar multiplication in a subspace of a Hilbert space.
|- (H e. SH -> ((A e. CC /\ B e. H) -> (A .h B) e. H))
Theorem	shsubclt 9043	Closure of vector subtraction in a subspace of a Hilbert space.
|- ((H e. SH /\ A e. H /\ B e. H) -> (A -h B) e. H)
Theorem	shsubcltOLD 9044	Closure of vector subtraction in a subspace of a Hilbert space.
|- (H e. SH -> ((A e. H /\ B e. H) -> (A -h B) e. H))
Theorem	sh2 9045	Subspace H of a Hilbert space.
|- (H (_ H~ -> (H e. SH <-> (0h e. H /\ (A.x e. H A.y e. H (x +h y) e. H /\ A.x e. CC A.y e. H (x .h y) e. H))))