P. 296 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29501-29600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	normsub 29501	Swapping order of subtraction doesn't change the norm of a vector. (Contributed by NM, 14-Aug-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) = (normℎ‘(𝐵 −ℎ 𝐴)))
Theorem	normneg 29502	The norm of a vector equals the norm of its negative. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normℎ‘(-1 ·ℎ 𝐴)) = (normℎ‘𝐴))
Theorem	normpyth 29503	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 → ((normℎ‘(𝐴 +ℎ 𝐵))↑2) = (((normℎ‘𝐴)↑2) + ((normℎ‘𝐵)↑2))))
Theorem	normpyc 29504	Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 → (normℎ‘𝐴) ≤ (normℎ‘(𝐴 +ℎ 𝐵))))
Theorem	norm3difi 29505	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐴 −ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ 𝐵)))
Theorem	norm3adifii 29506	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (abs‘((normℎ‘(𝐴 −ℎ 𝐶)) − (normℎ‘(𝐵 −ℎ 𝐶)))) ≤ (normℎ‘(𝐴 −ℎ 𝐵))
Theorem	norm3lem 29507	Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ (((normℎ‘(𝐴 −ℎ 𝐶)) < (𝐷 / 2) ∧ (normℎ‘(𝐶 −ℎ 𝐵)) < (𝐷 / 2)) → (normℎ‘(𝐴 −ℎ 𝐵)) < 𝐷)
Theorem	norm3dif 29508	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 20-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐴 −ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ 𝐵))))
Theorem	norm3dif2 29509	Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐶 −ℎ 𝐴)) + (normℎ‘(𝐶 −ℎ 𝐵))))
Theorem	norm3lemt 29510	Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℝ)) → (((normℎ‘(𝐴 −ℎ 𝐶)) < (𝐷 / 2) ∧ (normℎ‘(𝐶 −ℎ 𝐵)) < (𝐷 / 2)) → (normℎ‘(𝐴 −ℎ 𝐵)) < 𝐷))
Theorem	norm3adifi 29511	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 3-Oct-1999.) (New usage is discouraged.)
⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘((normℎ‘(𝐴 −ℎ 𝐶)) − (normℎ‘(𝐵 −ℎ 𝐶)))) ≤ (normℎ‘(𝐴 −ℎ 𝐵)))
Theorem	normpari 29512	Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (((normℎ‘(𝐴 −ℎ 𝐵))↑2) + ((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 · ((normℎ‘𝐴)↑2)) + (2 · ((normℎ‘𝐵)↑2)))
Theorem	normpar 29513	Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((normℎ‘(𝐴 −ℎ 𝐵))↑2) + ((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 · ((normℎ‘𝐴)↑2)) + (2 · ((normℎ‘𝐵)↑2))))
Theorem	normpar2i 29514	Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100. (Contributed by NM, 5-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((normℎ‘(𝐴 −ℎ 𝐵))↑2) = (((2 · ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (2 · ((normℎ‘(𝐵 −ℎ 𝐶))↑2))) − ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2 ·ℎ 𝐶)))↑2))
Theorem	polid2i 29515	Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ (𝐴 ·ih 𝐵) = (((((𝐴 +ℎ 𝐶) ·ih (𝐷 +ℎ 𝐵)) − ((𝐴 −ℎ 𝐶) ·ih (𝐷 −ℎ 𝐵))) + (i · (((𝐴 +ℎ (i ·ℎ 𝐶)) ·ih (𝐷 +ℎ (i ·ℎ 𝐵))) − ((𝐴 −ℎ (i ·ℎ 𝐶)) ·ih (𝐷 −ℎ (i ·ℎ 𝐵)))))) / 4)
Theorem	polidi 29516	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 29442. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ih 𝐵) = (((((normℎ‘(𝐴 +ℎ 𝐵))↑2) − ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i · (((normℎ‘(𝐴 +ℎ (i ·ℎ 𝐵)))↑2) − ((normℎ‘(𝐴 −ℎ (i ·ℎ 𝐵)))↑2)))) / 4)
Theorem	polid 29517	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 29442. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (((((normℎ‘(𝐴 +ℎ 𝐵))↑2) − ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i · (((normℎ‘(𝐴 +ℎ (i ·ℎ 𝐵)))↑2) − ((normℎ‘(𝐴 −ℎ (i ·ℎ 𝐵)))↑2)))) / 4))
19.2.3  Relate Hilbert space to normed complex vector spaces
Theorem	hilablo 29518	Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ +ℎ ∈ AbelOp
Theorem	hilid 29519	The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007.) (New usage is discouraged.)
⊢ (GId‘ +ℎ ) = 0ℎ
Theorem	hilvc 29520	Hilbert space is a complex vector space. Vector addition is +ℎ, and scalar product is ·ℎ. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ CVecOLD
Theorem	hilnormi 29521	Hilbert space norm in terms of vector space norm. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	hilhhi 29522	Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ +ℎ = ( +𝑣 ‘𝑈)    &   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
Theorem	hhnv 29523	Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	hhva 29524	The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	hhba 29525	The base set of Hilbert space. This theorem provides an independent proof of df-hba 29327 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ℋ = (BaseSet‘𝑈)
Theorem	hh0v 29526	The zero vector of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 0ℎ = (0vec‘𝑈)
Theorem	hhsm 29527	The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	hhvs 29528	The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ −ℎ = ( −𝑣 ‘𝑈)
Theorem	hhnm 29529	The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	hhims 29530	The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 = (IndMet‘𝑈)
Theorem	hhims2 29531	Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 = (normℎ ∘ −ℎ )
Theorem	hhmet 29532	The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 ∈ (Met‘ ℋ)
Theorem	hhxmet 29533	The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 ∈ (∞Met‘ ℋ)
Theorem	hhmetdval 29534	Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵)))
Theorem	hhip 29535	The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ·ih = (·𝑖OLD‘𝑈)
Theorem	hhph 29536	The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ CPreHilOLD
19.2.4  Bunjakovaskij-Cauchy-Schwarz inequality
Theorem	bcsiALT 29537	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵))
Theorem	bcsiHIL 29538	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Proved from ZFC version.) (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵))
Theorem	bcs 29539	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵)))
Theorem	bcs2 29540	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 29538. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐵))
Theorem	bcs3 29541	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 29538. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐵) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐴))
19.3  Cauchy sequences and completeness axiom
19.3.1  Cauchy sequences and limits
Theorem	hcau 29542*	Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝑥))
Theorem	hcauseq 29543	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 29544*	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 29545*	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 29546*	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 29547	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 29548	Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ)
Theorem	hlimconvi 29549*	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 29550*	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 29551*	Limit of the sum of two sequences in a Hilbert vector space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹:ℕ⟶ ℋ)    &   ⊢ (𝜑 → 𝐺:ℕ⟶ ℋ)    &   ⊢ (𝜑 → 𝐹 ⇝𝑣 𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝𝑣 𝐵)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛) +ℎ (𝐺‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝𝑣 (𝐴 +ℎ 𝐵))
19.3.2  Derivation of the completeness axiom from ZF set theory
Theorem	hilmet 29552	The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (Met‘ ℋ)
Theorem	hilxmet 29553	The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (∞Met‘ ℋ)
Theorem	hilmetdval 29554	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 29555	Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ +ℎ = ( +𝑣 ‘𝑈)    &   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝐷 = (normℎ ∘ −ℎ )
Theorem	hhcau 29556	The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑m ℕ))
Theorem	hhlm 29557	The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑m ℕ))
Theorem	hhcmpl 29558*	Lemma used for derivation of the completeness axiom ax-hcompl 29560 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥)    ⇒   ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
Theorem	hilcompl 29559*	Lemma used for derivation of the completeness axiom ax-hcompl 29560 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 29357; the 6th would be satisfied by eqid 2740; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl 29273. (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 → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
19.3.3  Completeness postulate for a Hilbert space
Axiom	ax-hcompl 29560*	Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
19.3.4  Relate Hilbert space to ZFC pre-Hilbert and Hilbert spaces
Theorem	hhcms 29561	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 29562	The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ CHilOLD
Theorem	hilcms 29563	The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (CMet‘ ℋ)
Theorem	hilhl 29564	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
19.4  Subspaces and projections
19.4.1  Subspaces
Definition	df-sh 29565	Define the set of subspaces of a Hilbert space. See issh 29566 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 29566	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 29567*	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 29568	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 29569	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 29570	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 29571	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 29572	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 29573	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 29574	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 29575	Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻)
Theorem	shmulcl 29576	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 29577*	Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻))))
Theorem	shsubcl 29578	Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 −ℎ 𝐵) ∈ 𝐻)
19.4.2  Closed subspaces
Definition	df-ch 29579	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 29580. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 29581 and isch3 29599. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.)
⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ}
Theorem	isch 29580	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 29581*	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 29582	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 29583	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 29584	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 29585	A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ 𝐻 ∈ Sℋ
Theorem	ch0 29586	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 29587	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 29588	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 29589	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 29590	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 29591	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 29592	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 29593	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 29594	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 29595	Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
Theorem	hlimuni 29596	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 29597*	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 29598*	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 29599*	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 29600*	Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥)