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	normne0 29501	A norm is nonzero iff its argument is a nonzero vector. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) ≠ 0 ↔ 𝐴 ≠ 0ℎ))
Theorem	normcli 29502	Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (normℎ‘𝐴) ∈ ℝ
Theorem	normsqi 29503	The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴)
Theorem	norm-i-i 29504	Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 5-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ)
Theorem	normsq 29505	The square of a norm. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴))
Theorem	normsub0i 29506	Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((normℎ‘(𝐴 −ℎ 𝐵)) = 0 ↔ 𝐴 = 𝐵)
Theorem	normsub0 29507	Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((normℎ‘(𝐴 −ℎ 𝐵)) = 0 ↔ 𝐴 = 𝐵))
Theorem	norm-ii-i 29508	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 +ℎ 𝐵)) ≤ ((normℎ‘𝐴) + (normℎ‘𝐵))
Theorem	norm-ii 29509	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 +ℎ 𝐵)) ≤ ((normℎ‘𝐴) + (normℎ‘𝐵)))
Theorem	norm-iii-i 29510	Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵))
Theorem	norm-iii 29511	Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵)))
Theorem	normsubi 29512	Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 −ℎ 𝐵)) = (normℎ‘(𝐵 −ℎ 𝐴))
Theorem	normpythi 29513	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	normsub 29514	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 29515	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 29516	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 29517	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 29518	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 29519	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 29520	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 29521	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 29522	Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐶 −ℎ 𝐴)) + (normℎ‘(𝐶 −ℎ 𝐵))))
Theorem	norm3lemt 29523	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 29524	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 29525	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 29526	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 29527	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 29528	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 29529	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 29455. (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 29530	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 29455. (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 29531	Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ +ℎ ∈ AbelOp
Theorem	hilid 29532	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 29533	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 29534	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 29535	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 29536	Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	hhva 29537	The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	hhba 29538	The base set of Hilbert space. This theorem provides an independent proof of df-hba 29340 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ℋ = (BaseSet‘𝑈)
Theorem	hh0v 29539	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 29540	The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	hhvs 29541	The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ −ℎ = ( −𝑣 ‘𝑈)
Theorem	hhnm 29542	The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	hhims 29543	The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 = (IndMet‘𝑈)
Theorem	hhims2 29544	Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 = (normℎ ∘ −ℎ )
Theorem	hhmet 29545	The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 ∈ (Met‘ ℋ)
Theorem	hhxmet 29546	The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 ∈ (∞Met‘ ℋ)
Theorem	hhmetdval 29547	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 29548	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 29549	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 29550	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 29551	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 29552	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 29553	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 29551. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐵))
Theorem	bcs3 29554	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 29551. (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 29555*	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 29556	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 29557*	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 29558*	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 29559*	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 29560	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 29561	Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ)
Theorem	hlimconvi 29562*	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 29563*	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 29564*	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 29565	The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (Met‘ ℋ)
Theorem	hilxmet 29566	The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (∞Met‘ ℋ)
Theorem	hilmetdval 29567	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 29568	Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ +ℎ = ( +𝑣 ‘𝑈)    &   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝐷 = (normℎ ∘ −ℎ )
Theorem	hhcau 29569	The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑m ℕ))
Theorem	hhlm 29570	The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑m ℕ))
Theorem	hhcmpl 29571*	Lemma used for derivation of the completeness axiom ax-hcompl 29573 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥)    ⇒   ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
Theorem	hilcompl 29572*	Lemma used for derivation of the completeness axiom ax-hcompl 29573 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 29370; the 6th would be satisfied by eqid 2739; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl 29286. (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 29573*	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 29574	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 29575	The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ CHilOLD
Theorem	hilcms 29576	The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 ∈ (CMet‘ ℋ)
Theorem	hilhl 29577	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 29578	Define the set of subspaces of a Hilbert space. See issh 29579 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 29579	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 29580*	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 29581	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 29582	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 29583	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 29584	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 29585	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 29586	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 29587	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 29588	Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻)
Theorem	shmulcl 29589	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 29590*	Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻))))
Theorem	shsubcl 29591	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 29592	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 29593. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 29594 and isch3 29612. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.)
⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ}
Theorem	isch 29593	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 29594*	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 29595	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 29596	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 29597	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 29598	A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ 𝐻 ∈ Sℋ
Theorem	ch0 29599	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 29600	A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → 𝐻 ⊆ ℋ)