mmtheorems94 - 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 - 9301-9400 - Page 94 of 123

Type	Label	Description
Statement
Theorem	polidi 9301	Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of axiom ax-his3 9227.
|- A e. H~   &   |- B e. H~   =>   |- (A .ih B) = (((((normh` (A +h B))^2) - ((normh` (A -h B))^2)) + (i x. (((normh` (A +h (i .h B)))^2) - ((normh` (A -h (i .h B)))^2)))) / 4)
Theorem	polid 9302	Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of axiom ax-his3 9227.
|- ((A e. H~ /\ B e. H~) -> (A .ih B) = (((((normh` (A +h B))^2) - ((normh` (A -h B))^2)) + (i x. (((normh` (A +h (i .h B)))^2) - ((normh` (A -h (i .h B)))^2)))) / 4))
Relate Hilbert space to normed complex vector spaces
Theorem	hilabl 9303	Hilbert space vector addition is an Abelian group operation.
|- +h e. Abel
Theorem	hilid 9304	The group identity element of Hilbert space vector addition is the zero vector.
|- (Id` +h ) = 0h
Theorem	hilvc 9305	Hilbert space is a complex vector space. Vector addition is +h, and scalar product is .h.
|- <. +h , .h >. e. CVec
Theorem	hilnormi 9306	Hilbert space norm in terms of vector space norm.
|- H~ = (BaseSet` U)   &   |- .ih = (.i` U)   &   |- U e. NrmCVec   =>   |- normh = (norm` U)
Theorem	hilhhi 9307	Deduce the structure of Hilbert space from its components.
|- H~ = (BaseSet` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- U e. NrmCVec   =>   |- U = <.<. +h , .h >., normh>.
Theorem	hhnv 9308	Hilbert space is a normed complex vector space.
|- U = <.<. +h , .h >., normh>.   =>   |- U e. NrmCVec
Theorem	hhva 9309	The group (addition) operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- +h = (+v` U)
Theorem	hhba 9310	The base set of Hilbert space. This theorem provides an independent proof of df-hba 9113 (see comments in that definition).
|- U = <.<. +h , .h >., normh>.   =>   |- H~ = (BaseSet` U)
Theorem	hh0v 9311	The zero vector of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- 0h = (0v` U)
Theorem	hhsm 9312	The scalar product operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- .h = (.s` U)
Theorem	hhvs 9313	The vector subtraction operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- -h = (-v` U)
Theorem	hhnm 9314	The norm function of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- normh = (norm` U)
Theorem	hhims 9315	The induced metric of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (normh o. -h )   =>   |- D = (IndMet` U)
Theorem	hhims2 9316	Hilbert space distance metric.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- D = (normh o. -h )
Theorem	hhmet 9317	The induced metric of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- D e. Met
Theorem	hhmetba 9318	The base set for the metric for Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- H~ = dom dom D
Theorem	hhmetdval 9319	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 9320	The inner product operation of Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- .ih = (.i` U)
Theorem	hhph 9321	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	bcsiALT 9322	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	bcsiHIL 9323	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	bcs 9324	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	bcs2 9325	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 9323.
|- ((A e. H~ /\ B e. H~ /\ (normh` A) <_ 1) -> (abs` (A .ih B)) <_ (normh` B))
Theorem	bcs3 9326	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 9323.
|- ((A e. H~ /\ B e. H~ /\ (normh` B) <_ 1) -> (abs` (A .ih B)) <_ (normh` A))
Cauchy sequences and limits
Theorem	hcau 9327	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 9328	A Cauchy sequences on a Hilbert space is a sequence.
|- (F e. Cauchy -> F:NN-->H~)
Theorem	hcaucvg 9329	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 9330	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 9331	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	hlimi 9332	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	hlimseqi 9333	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	hlimveci 9334	Closure of the limit of a sequence on Hilbert space.
|- F e. V   &   |- A e. V   =>   |- (F ~~>v A -> A e. H~)
Theorem	hlimconvi 9335	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 9336	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 9337	The Hilbert space norm determines a metric space.
|- D = (normh o. -h )   =>   |- D e. Met
Theorem	hilmetdval 9338	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 9339	The base set for the metric for Hilbert space.
|- D = (normh o. -h )   =>   |- H~ = dom dom D
Theorem	hilims 9340	Hilbert space distance metric.
|- H~ = (BaseSet` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- D = (IndMet` U)   &   |- U e. NrmCVec   =>   |- D = (normh o. -h )
Theorem	hillim 9341	Hilbert space limit in terms of metric space limit.
|- H~ = (BaseSet` U)   &   |- +h = (+v` U)   &   |- .h = (.s` U)   &   |- .ih = (.i` U)   &   |- D = (IndMet` U)   &   |- U e. NrmCVec   =>   |- ~~>v = ((~~>m` D) |` (H~ ^m NN))
Theorem	hilcau 9342	Hilbert space Cauchy sequences in terms of metric space Cauchy sequences.
|- H~ = (BaseSet` 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 9343	The limit sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- ~~>v = ((~~>m` D) |` (H~ ^m NN))
Theorem	hhcau 9344	The Cauchy sequences of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- Cauchy = ((Cau` D) i^i (H~ ^m NN))
Theorem	hhcmpl 9345	Lemma used for derivation of the completeness axiom ax-hcompl 9347 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 9346	Lemma used for derivation of the completeness axiom ax-hcompl 9347 from ZFC Hilbert space theory. The first 5 hypotheses would be satisfied by the definitions described in ax-hilex 9144; the 6th would be satisfied by eqid 1518; the 7th by a given fixed Hilbert space; and the last by theorem hlcompl 8879.
|- H~ = (BaseSet` 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 9347	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 9348	The Hilbert space induced metric determines a complete metric space.
|- U = <.<. +h , .h >., normh>.   &   |- D = (IndMet` U)   =>   |- D e. CMet
Theorem	hhhl 9349	The Hilbert space structure is a complex Hilbert space.
|- U = <.<. +h , .h >., normh>.   =>   |- U e. CHil
Theorem	hilcms 9350	The Hilbert space norm determines a complete metric space.
|- D = (normh o. -h )   =>   |- D e. CMet
Theorem	hilhl 9351	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 9352	Define the set of subspaces of a Hilbert space. See sh 9354 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 9353	The set of subspaces of a Hilbert space exists (is a set).
|- SH e. V
Theorem	sh 9354	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 9355	A subspace is a subset of Hilbert space.
|- (H e. SH -> H (_ H~)
Theorem	shel 9356	A member of a subspace of a Hilbert space is a vector.
|- ((H e. SH /\ A e. H) -> A e. H~)
Theorem	shssii 9357	A closed subspace of a Hilbert space is a subset of Hilbert space.
|- H e. SH   =>   |- H (_ H~
Theorem	sheli 9358	A member of a subspace of a Hilbert space is a vector.
|- H e. SH   =>   |- (A e. H -> A e. H~)
Theorem	shelii 9359	A member of a subspace of a Hilbert space is a vector.
|- H e. SH   &   |- A e. H   =>   |- A e. H~
Theorem	sh0 9360	The zero vector belongs to any subspace of a Hilbert space.
|- (H e. SH -> 0h e. H)
Theorem	shaddcl 9361	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	shaddclOLD 9362	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	shmulcl 9363	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	shmulclOLD 9364	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	shsubcl 9365	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	shsubclOLD 9366	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 9367	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))))
Closed subspaces
Definition	df-ch 9368	Define the set of closed subspaces of a Hilbert space. A closed subspace is one in which the limit of every convergent sequence in the subspace belongs to the subspace. For its membership relation, see closedsub 9369. From Definition of [Beran] p. 107. Alternate definitions are given by chcmhi 9389 and dfch2 9525.
|- CH = {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}
Theorem	closedsub 9369	Closed subspace H of a Hilbert space. Definition of [Beran] p. 107.
|- (H e. CH <-> (H e. SH /\ A.fA.x((f:NN-->H /\ f ~~>v x) -> x e. H)))
Theorem	chsssh 9370	Closed subspaces are subspaces in a Hilbert space.
|- CH (_ SH
Theorem	chex 9371	The set of closed subspaces of a Hilbert space exists (is a set).
|- CH e. V
Theorem	chsh 9372	A closed subspace is a subspace.
|- (H e. CH -> H e. SH)
Theorem	chshii 9373	A closed subspace is a subspace.
|- H e. CH   =>   |- H e. SH
Theorem	ch0 9374	The zero vector belongs to any closed subspace of a Hilbert space.
|- (H e. CH -> 0h e. H)
Theorem	chss 9375	A closed subspace of a Hilbert space is a subset of Hilbert space.
|- (H e. CH -> H (_ H~)
Theorem	chel 9376	A member of a closed subspace of a Hilbert space is a vector.
|- ((H e. CH /\ A e. H) -> A e. H~)
Theorem	chssii 9377	A closed subspace of a Hilbert space is a subset of Hilbert space.
|- H e. CH   =>   |- H (_ H~
Theorem	cheli 9378	A member of a closed subspace of a Hilbert space is a vector.
|- H e. CH   =>   |- (A e. H -> A e. H~)
Theorem	chelii 9379	A member of a closed subspace of a Hilbert space is a vector.
|- H e. CH   &   |- A e. H   =>   |- A e. H~
Theorem	chlimi 9380	The limit property of a closed subspace of a Hilbert space.
|- A e. V   =>   |- ((H e. CH /\ F:NN-->H /\ F ~~>v A) -> A e. H)
Theorem	hlim0 9381	The zero sequence in Hilbert space converges to the zero vector.
|- (NN X. {0h}) ~~>v 0h
Theorem	hlimcauii 9382	If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence.
|- A e. V   &   |- F e. V   &   |- F ~~>v A   =>   |- F e. Cauchy
Theorem	hlimcaui 9383	If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence.
|- A e. V   &   |- F e. V   =>   |- (F ~~>v A -> F e. Cauchy)
Theorem	hlimuniii 9384	A Hilbert space sequence converges to at most one limit.
|- A e. V   &   |- B e. V   &   |- F e. V   &   |- (F ~~>v A /\ F ~~>v B)   =>   |- A = B
Theorem	hlimunii 9385	A Hilbert space sequence converges to at most one limit.
|- A e. V   &   |- B e. V   &   |- F e. V   =>   |- ((F ~~>v A /\ F ~~>v B) -> A = B)
Theorem	hlimreui 9386	The limit of a Hilbert space sequence is unique.
|- F e. V   =>   |- (E.x e. H F ~~>v x <-> E!x e. H F ~~>v x)
Theorem	hlimeui 9387	The limit of a Hilbert space sequence is unique.
|- F e. V   =>   |- (E.x F ~~>v x <-> E!x F ~~>v x)
Theorem	chsscmi 9388	The hypothesis defines the set of complete subspaces of Hilbert space. A complete subspace is one in which every Cauchy sequence of vectors in the subspace converges to a member of the subspace (Definition of complete subspace in [Beran] p. 96). Any closed subspace of a Hilbert space is complete. Part of Remark 3.12 of [Beran] p. 107.
|- C = {h | (h e. SH /\ A.f e. Cauchy (f:NN-->h -> E.x e. h f ~~>v x))}   =>   |- CH (_ C
Theorem	chcmhi 9389	The hypothesis defines the set of complete subspaces of Hilbert space (see chsscmi 9388). A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107.
|- C = {h | (h e. SH /\ A.f e. Cauchy (f:NN-->h -> E.x e. h f ~~>v x))}   =>   |- CH = C
Theorem	ch2 9390	A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107.
|- (H e. CH <-> (H e. SH /\ A.f e. Cauchy (f:NN-->H -> E.x e. H f ~~>v x)))
Theorem	chcompl 9391	Completeness of a closed subspace of Hilbert space.
|- ((H e. CH /\ F e. Cauchy /\ F:NN-->H) -> E.x e. H F ~~>v x)
Theorem	helch 9392	The unit Hilbert lattice element (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65.
|- H~ e. CH
Theorem	helsh 9393	Hilbert space is a subspace of Hilbert space.
|- H~ e. SH
Theorem	shsspwh 9394	Subspaces are subsets of Hilbert space.
|- SH (_ P~H~
Theorem	chsspwh 9395	Closed subspaces are subsets of Hilbert space.
|- CH (_ P~H~
Theorem	hsn0elch 9396	The zero subspace belongs to the set of closed subspaces of Hilbert space.
|- {0h} e. CH
Theorem	norm1 9397	From any nonzero Hilbert space vector, construct a vector whose norm is 1.
|- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h A)) = 1)
Theorem	norm1exi 9398	A normalized vector exists in a subspace iff the subspace has a non-zero vector.
|- H e. SH   =>   |- (E.x e. H x =/= 0h <-> E.y e. H (normh` y) = 1)
Theorem	norm1hex 9399	A normalized vector can exist only iff the Hilbert space has a non-zero vector.
|- (E.x e. H~ x =/= 0h <-> E.y e. H~ (normh` y) = 1)
Orthocomplements
Definition	df-oc 9400	Define orthogonal complement of a subset (usually a subspace) of Hilbert space. The orthogonal complement is the set of all vectors orthogonal to all vectors in the subset. See ocval 9429 and chocvali 9447 for its value. Textbooks usually denote this unary operation with the symbol _|_ as a small superscript, although Mittelstaedt uses the symbol as a prefix operation. Here we define a function (prefix operation) _|_ rather than introducing a new syntactical form. This lets us take advantage of the theorems about functions that we already have proved under set theory. Definition of [Mittelstaedt] p. 9.
|- _|_ = {<.x, y>. | (x (_ H~ /\ y = {z e. H~ | A.w e. x (z .ih w) = 0})}