P. 304 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30301-30400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hcauseq 30301	A Cauchy sequences on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐹 ∈ Cauchy → 𝐹:ℕ⟶ ℋ)
Theorem	hcaucvg 30302*	A Cauchy sequence on a Hilbert space converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ((𝐹 ∈ Cauchy ∧ 𝐴 ∈ ℝ+) → ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝐴)
Theorem	seq1hcau 30303*	A sequence on a Hilbert space is a Cauchy sequence if it converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐹:ℕ⟶ ℋ → (𝐹 ∈ Cauchy ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝑥))
Theorem	hlimi 30304*	Express the predicate: The limit of vector sequence 𝐹 in a Hilbert space is 𝐴, i.e. 𝐹 converges to 𝐴. This means that for any real 𝑥, no matter how small, there always exists an integer 𝑦 such that the norm of any later vector in the sequence minus the limit is less than 𝑥. Definition of converge in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 ⇝𝑣 𝐴 ↔ ((𝐹:ℕ⟶ ℋ ∧ 𝐴 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑧) −ℎ 𝐴)) < 𝑥))
Theorem	hlimseqi 30305	A sequence with a limit on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐹:ℕ⟶ ℋ)
Theorem	hlimveci 30306	Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ)
Theorem	hlimconvi 30307*	Convergence of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐹 ⇝𝑣 𝐴 ∧ 𝐵 ∈ ℝ+) → ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑧) −ℎ 𝐴)) < 𝐵)
Theorem	hlim2 30308*	The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ((𝐹:ℕ⟶ ℋ ∧ 𝐴 ∈ ℋ) → (𝐹 ⇝𝑣 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑧) −ℎ 𝐴)) < 𝑥))
Theorem	hlimadd 30309*	Limit of the sum of two sequences in a Hilbert vector space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹:ℕ⟶ ℋ)    &   ⊢ (𝜑 → 𝐺:ℕ⟶ ℋ)    &   ⊢ (𝜑 → 𝐹 ⇝𝑣 𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝𝑣 𝐵)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛) +ℎ (𝐺‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝𝑣 (𝐴 +ℎ 𝐵))
20.3.2  Derivation of the completeness axiom from ZF set theory
Theorem	hilmet 30310	The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (Met‘ ℋ)
Theorem	hilxmet 30311	The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (∞Met‘ ℋ)
Theorem	hilmetdval 30312	Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵)))
Theorem	hilims 30313	Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ +ℎ = ( +𝑣 ‘𝑈)    &   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝐷 = (normℎ ∘ −ℎ )
Theorem	hhcau 30314	The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑m ℕ))
Theorem	hhlm 30315	The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑m ℕ))
Theorem	hhcmpl 30316*	Lemma used for derivation of the completeness axiom ax-hcompl 30318 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥)    ⇒   ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
Theorem	hilcompl 30317*	Lemma used for derivation of the completeness axiom ax-hcompl 30318 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 30115; the 6th would be satisfied by eqid 2731; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl 30031. (Contributed by NM, 13-Sep-2007.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ +ℎ = ( +𝑣 ‘𝑈)    &   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥)    ⇒   ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
20.3.3  Completeness postulate for a Hilbert space
Axiom	ax-hcompl 30318*	Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
20.3.4  Relate Hilbert space to ZFC pre-Hilbert and Hilbert spaces
Theorem	hhcms 30319	The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008.) (Proof shortened by Mario Carneiro, 14-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 ∈ (CMet‘ ℋ)
Theorem	hhhl 30320	The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ CHilOLD
Theorem	hilcms 30321	The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (CMet‘ ℋ)
Theorem	hilhl 30322	The Hilbert space of the Hilbert Space Explorer is a complex Hilbert space. (Contributed by Steve Rodriguez, 29-Apr-2007.) (New usage is discouraged.)
⊢ ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ∈ CHilOLD
20.4  Subspaces and projections
20.4.1  Subspaces
Definition	df-sh 30323	Define the set of subspaces of a Hilbert space. See issh 30324 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. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ Sℋ = {ℎ ∈ 𝒫 ℋ ∣ (0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ “ (ℂ × ℎ)) ⊆ ℎ)}
Theorem	issh 30324	Subspace 𝐻 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. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻)))
Theorem	issh2 30325*	Subspace 𝐻 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. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))
Theorem	shss 30326	A subspace is a subset of Hilbert space. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ)
Theorem	shel 30327	A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻) → 𝐴 ∈ ℋ)
Theorem	shex 30328	The set of subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ Sℋ ∈ V
Theorem	shssii 30329	A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐻 ⊆ ℋ
Theorem	sheli 30330	A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)
Theorem	shelii 30331	A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐴 ∈ 𝐻    ⇒   ⊢ 𝐴 ∈ ℋ
Theorem	sh0 30332	The zero vector belongs to any subspace of a Hilbert space. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → 0ℎ ∈ 𝐻)
Theorem	shaddcl 30333	Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻)
Theorem	shmulcl 30334	Closure of vector scalar multiplication in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ℎ 𝐵) ∈ 𝐻)
Theorem	issh3 30335*	Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻))))
Theorem	shsubcl 30336	Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 −ℎ 𝐵) ∈ 𝐻)
20.4.2  Closed subspaces
Definition	df-ch 30337	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 isch 30338. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 30339 and isch3 30357. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.)
⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ}
Theorem	isch 30338	Closed subspace 𝐻 of a Hilbert space. (Contributed by NM, 17-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ ↔ (𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ (𝐻 ↑m ℕ)) ⊆ 𝐻))
Theorem	isch2 30339*	Closed subspace 𝐻 of a Hilbert space. Definition of [Beran] p. 107. (Contributed by NM, 17-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ ↔ (𝐻 ∈ Sℋ ∧ ∀𝑓∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻)))
Theorem	chsh 30340	A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
Theorem	chsssh 30341	Closed subspaces are subspaces in a Hilbert space. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ Cℋ ⊆ Sℋ
Theorem	chex 30342	The set of closed subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ Cℋ ∈ V
Theorem	chshii 30343	A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ 𝐻 ∈ Sℋ
Theorem	ch0 30344	The zero vector belongs to any closed subspace of a Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → 0ℎ ∈ 𝐻)
Theorem	chss 30345	A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → 𝐻 ⊆ ℋ)
Theorem	chel 30346	A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻) → 𝐴 ∈ ℋ)
Theorem	chssii 30347	A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ 𝐻 ⊆ ℋ
Theorem	cheli 30348	A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)
Theorem	chelii 30349	A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ 𝐻    ⇒   ⊢ 𝐴 ∈ ℋ
Theorem	chlimi 30350	The limit property of a closed subspace of a Hilbert space. (Contributed by NM, 14-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐻 ∈ Cℋ ∧ 𝐹:ℕ⟶𝐻 ∧ 𝐹 ⇝𝑣 𝐴) → 𝐴 ∈ 𝐻)
Theorem	hlim0 30351	The zero sequence in Hilbert space converges to the zero vector. (Contributed by NM, 17-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (ℕ × {0ℎ}) ⇝𝑣 0ℎ
Theorem	hlimcaui 30352	If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. (Contributed by NM, 17-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐹 ⇝𝑣 𝐴 → 𝐹 ∈ Cauchy)
Theorem	hlimf 30353	Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
Theorem	hlimuni 30354	A Hilbert space sequence converges to at most one limit. (Contributed by NM, 19-Aug-1999.) (Revised by Mario Carneiro, 2-May-2015.) (New usage is discouraged.)
⊢ ((𝐹 ⇝𝑣 𝐴 ∧ 𝐹 ⇝𝑣 𝐵) → 𝐴 = 𝐵)
Theorem	hlimreui 30355*	The limit of a Hilbert space sequence is unique. (Contributed by NM, 19-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥 ↔ ∃!𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥)
Theorem	hlimeui 30356*	The limit of a Hilbert space sequence is unique. (Contributed by NM, 19-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (∃𝑥 𝐹 ⇝𝑣 𝑥 ↔ ∃!𝑥 𝐹 ⇝𝑣 𝑥)
Theorem	isch3 30357*	A Hilbert subspace is closed iff it is complete. 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). Remark 3.12 of [Beran] p. 107. (Contributed by NM, 24-Dec-2001.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ ↔ (𝐻 ∈ Sℋ ∧ ∀𝑓 ∈ Cauchy (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)))
Theorem	chcompl 30358*	Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥)
Theorem	helch 30359	The Hilbert lattice one (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 6-Sep-1999.) (New usage is discouraged.)
⊢ ℋ ∈ Cℋ
Theorem	ifchhv 30360	Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.)
⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ
Theorem	helsh 30361	Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ℋ ∈ Sℋ
Theorem	shsspwh 30362	Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Sℋ ⊆ 𝒫 ℋ
Theorem	chsspwh 30363	Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Cℋ ⊆ 𝒫 ℋ
Theorem	hsn0elch 30364	The zero subspace belongs to the set of closed subspaces of Hilbert space. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ {0ℎ} ∈ Cℋ
Theorem	norm1 30365	From any nonzero Hilbert space vector, construct a vector whose norm is 1. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (normℎ‘((1 / (normℎ‘𝐴)) ·ℎ 𝐴)) = 1)
Theorem	norm1exi 30366*	A normalized vector exists in a subspace iff the subspace has a nonzero vector. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ (∃𝑥 ∈ 𝐻 𝑥 ≠ 0ℎ ↔ ∃𝑦 ∈ 𝐻 (normℎ‘𝑦) = 1)
Theorem	norm1hex 30367	A normalized vector can exist only iff the Hilbert space has a nonzero vector. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ ℋ 𝑥 ≠ 0ℎ ↔ ∃𝑦 ∈ ℋ (normℎ‘𝑦) = 1)
20.4.3  Orthocomplements
Definition	df-oc 30368*	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 30396 and chocvali 30415 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 syntactic form. This lets us take advantage of the theorems about functions that we already have proved under set theory. Definition of [Mittelstaedt] p. 9. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ ⊥ = (𝑥 ∈ 𝒫 ℋ ↦ {𝑦 ∈ ℋ ∣ ∀𝑧 ∈ 𝑥 (𝑦 ·ih 𝑧) = 0})
Definition	df-ch0 30369	Define the zero for closed subspaces of Hilbert space. See h0elch 30371 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ 0ℋ = {0ℎ}
Theorem	elch0 30370	Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.)
⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ)
Theorem	h0elch 30371	The zero subspace is a closed subspace. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ 0ℋ ∈ Cℋ
Theorem	h0elsh 30372	The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ 0ℋ ∈ Sℋ
Theorem	hhssva 30373	The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊)
Theorem	hhsssm 30374	The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊)
Theorem	hhssnm 30375	The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊)
Theorem	issubgoilem 30376*	Lemma for hhssabloilem 30377. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵))
Theorem	hhssabloilem 30377	Lemma for hhssabloi 30378. Formerly part of proof for hhssabloi 30378 which was based on the deprecated definition "SubGrpOp" for subgroups. (Contributed by NM, 9-Apr-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (Revised by AV, 27-Aug-2021.) (New usage is discouraged.)
⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( +ℎ ∈ GrpOp ∧ ( +ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ ( +ℎ ↾ (𝐻 × 𝐻)) ⊆ +ℎ )
Theorem	hhssabloi 30378	Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (Proof shortened by AV, 27-Aug-2021.) (New usage is discouraged.)
⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp
Theorem	hhssablo 30379	Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp)
Theorem	hhssnv 30380	Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝑊 ∈ NrmCVec
Theorem	hhssnvt 30381	Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec)
Theorem	hhsst 30382	A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈))
Theorem	hhshsslem1 30383	Lemma for hhsssh 30385. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhshsslem2 30384	Lemma for hhsssh 30385. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 ∈ Sℋ
Theorem	hhsssh 30385	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ))
Theorem	hhsssh2 30386	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ))
Theorem	hhssba 30387	The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhssvs 30388	The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊)
Theorem	hhssvsf 30389	Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻
Theorem	hhssims 30390	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))    ⇒   ⊢ 𝐷 = (IndMet‘𝑊)
Theorem	hhssims2 30391	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))
Theorem	hhssmet 30392	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 ∈ (Met‘𝐻)
Theorem	hhssmetdval 30393	Value of the distance function of the metric space of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵)))
Theorem	hhsscms 30394	The induced metric of a closed subspace is complete. (Contributed by NM, 10-Apr-2008.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ 𝐷 ∈ (CMet‘𝐻)
Theorem	hhssbnOLD 30395	Obsolete version of cssbn 24821: Banach space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ 𝑊 ∈ CBan
Theorem	ocval 30396*	Value of orthogonal complement of a subset of Hilbert space. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (⊥‘𝐻) = {𝑥 ∈ ℋ ∣ ∀𝑦 ∈ 𝐻 (𝑥 ·ih 𝑦) = 0})
Theorem	ocel 30397*	Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	shocel 30398*	Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	ocsh 30399	The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ∈ Sℋ )
Theorem	shocsh 30400	The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ∈ Sℋ )