P. 297 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29601-29700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chel 29601	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 29602	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 29603	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 29604	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 29605	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 29606	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 29607	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 29608	Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
Theorem	hlimuni 29609	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 29610*	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 29611*	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 29612*	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 29613*	Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥)
Theorem	helch 29614	The unit Hilbert lattice element (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 29615	Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.)
⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ
Theorem	helsh 29616	Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ℋ ∈ Sℋ
Theorem	shsspwh 29617	Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Sℋ ⊆ 𝒫 ℋ
Theorem	chsspwh 29618	Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Cℋ ⊆ 𝒫 ℋ
Theorem	hsn0elch 29619	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 29620	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 29621*	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 29622	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)
19.4.3  Orthocomplements
Definition	df-oc 29623*	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 29651 and chocvali 29670 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 29624	Define the zero for closed subspaces of Hilbert space. See h0elch 29626 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ 0ℋ = {0ℎ}
Theorem	elch0 29625	Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.)
⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ)
Theorem	h0elch 29626	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 29627	The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ 0ℋ ∈ Sℋ
Theorem	hhssva 29628	The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊)
Theorem	hhsssm 29629	The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊)
Theorem	hhssnm 29630	The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊)
Theorem	issubgoilem 29631*	Lemma for hhssabloilem 29632. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵))
Theorem	hhssabloilem 29632	Lemma for hhssabloi 29633. Formerly part of proof for hhssabloi 29633 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 29633	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 29634	Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp)
Theorem	hhssnv 29635	Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝑊 ∈ NrmCVec
Theorem	hhssnvt 29636	Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec)
Theorem	hhsst 29637	A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈))
Theorem	hhshsslem1 29638	Lemma for hhsssh 29640. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhshsslem2 29639	Lemma for hhsssh 29640. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 ∈ Sℋ
Theorem	hhsssh 29640	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ))
Theorem	hhsssh2 29641	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ))
Theorem	hhssba 29642	The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhssvs 29643	The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊)
Theorem	hhssvsf 29644	Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻
Theorem	hhssims 29645	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))    ⇒   ⊢ 𝐷 = (IndMet‘𝑊)
Theorem	hhssims2 29646	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))
Theorem	hhssmet 29647	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 ∈ (Met‘𝐻)
Theorem	hhssmetdval 29648	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 29649	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 29650	Obsolete version of cssbn 24548: 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 29651*	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 29652*	Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	shocel 29653*	Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	ocsh 29654	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 29655	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ℋ )
Theorem	ocss 29656	An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ⊆ ℋ)
Theorem	shocss 29657	An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ⊆ ℋ)
Theorem	occon 29658	Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘𝐵) ⊆ (⊥‘𝐴)))
Theorem	occon2 29659	Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵))))
Theorem	occon2i 29660	Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ 𝐴 ⊆ ℋ    &   ⊢ 𝐵 ⊆ ℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵)))
Theorem	oc0 29661	The zero vector belongs to an orthogonal complement of a Hilbert subspace. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → 0ℎ ∈ (⊥‘𝐻))
Theorem	ocorth 29662	Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0))
Theorem	shocorth 29663	Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0))
Theorem	ococss 29664	Inclusion in complement of complement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (⊥‘(⊥‘𝐴)))
Theorem	shococss 29665	Inclusion in complement of complement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → 𝐴 ⊆ (⊥‘(⊥‘𝐴)))
Theorem	shorth 29666	Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → (𝐺 ⊆ (⊥‘𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ih 𝐵) = 0)))
Theorem	ocin 29667	Intersection of a Hilbert subspace and its complement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ)
Theorem	occon3 29668	Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴)))
Theorem	ocnel 29669	A nonzero vector in the complement of a subspace does not belong to the subspace. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ (⊥‘𝐻) ∧ 𝐴 ≠ 0ℎ) → ¬ 𝐴 ∈ 𝐻)
Theorem	chocvali 29670*	Value of the orthogonal complement of a Hilbert lattice element. The orthogonal complement of 𝐴 is the set of vectors that are orthogonal to all vectors in 𝐴. (Contributed by NM, 8-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) = {𝑥 ∈ ℋ ∣ ∀𝑦 ∈ 𝐴 (𝑥 ·ih 𝑦) = 0}
Theorem	shuni 29671	Two subspaces with trivial intersection have a unique decomposition of the elements of the subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐻 ∈ Sℋ )    &   ⊢ (𝜑 → 𝐾 ∈ Sℋ )    &   ⊢ (𝜑 → (𝐻 ∩ 𝐾) = 0ℋ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐻)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐻)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐾)    &   ⊢ (𝜑 → (𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	chocunii 29672	Lemma for uniqueness part of Projection Theorem. Theorem 3.7(i) of [Beran] p. 102 (uniqueness part). (Contributed by NM, 23-Oct-1999.) (Proof shortened by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) → ((𝑅 = (𝐴 +ℎ 𝐵) ∧ 𝑅 = (𝐶 +ℎ 𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	pjhthmo 29673*	Projection Theorem, uniqueness part. Any two disjoint subspaces yield a unique decomposition of vectors into each subspace. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)))
Theorem	occllem 29674	Lemma for occl 29675. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ⊆ ℋ)    &   ⊢ (𝜑 → 𝐹 ∈ Cauchy)    &   ⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (( ⇝𝑣 ‘𝐹) ·ih 𝐵) = 0)
Theorem	occl 29675	Closure of complement of Hilbert subset. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 8-Aug-2000.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ∈ Cℋ )
Theorem	shoccl 29676	Closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ∈ Cℋ )
Theorem	choccl 29677	Closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → (⊥‘𝐴) ∈ Cℋ )
Theorem	choccli 29678	Closure of Cℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) ∈ Cℋ
19.4.4  Subspace sum, span, lattice join, lattice supremum
Definition	df-shs 29679*	Define subspace sum in Sℋ. See shsval 29683, shsval2i 29758, and shsval3i 29759 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦)))
Definition	df-span 29680*	Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 29704 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ span = (𝑥 ∈ 𝒫 ℋ ↦ ∩ {𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦})
Definition	df-chj 29681*	Define Hilbert lattice join. See chjval 29723 for its value and chjcl 29728 for its closure law. Note that we define it over all Hilbert space subsets to allow proving more general theorems. Even for general subsets the join belongs to Cℋ; see sshjcl 29726. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦))))
Definition	df-chsup 29682	Define the supremum of a set of Hilbert lattice elements. See chsupval2 29781 for its value. We actually define the supremum for an arbitrary collection of Hilbert space subsets, not just elements of the Hilbert lattice Cℋ, to allow more general theorems. Even for general subsets the supremum still a Hilbert lattice element; see hsupcl 29710. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.)
⊢ ∨ℋ = (𝑥 ∈ 𝒫 𝒫 ℋ ↦ (⊥‘(⊥‘∪ 𝑥)))
Theorem	shsval 29683	Value of subspace sum of two Hilbert space subspaces. Definition of subspace sum in [Kalmbach] p. 65. (Contributed by NM, 16-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) = ( +ℎ “ (𝐴 × 𝐵)))
Theorem	shsss 29684	The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ⊆ ℋ)
Theorem	shsel 29685*	Membership in the subspace sum of two Hilbert subspaces. (Contributed by NM, 14-Dec-2004.) (Revised by Mario Carneiro, 29-Jan-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)))
Theorem	shsel3 29686*	Membership in the subspace sum of two Hilbert subspaces, using vector subtraction. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦)))
Theorem	shseli 29687*	Membership in subspace sum. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))
Theorem	shscli 29688	Closure of subspace sum. (Contributed by NM, 15-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) ∈ Sℋ
Theorem	shscl 29689	Closure of subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ∈ Sℋ )
Theorem	shscom 29690	Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴))
Theorem	shsva 29691	Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsel1 29692	A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ 𝐴 → 𝐶 ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsel2 29693	A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ 𝐵 → 𝐶 ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsvs 29694	Vector subtraction belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsub1 29695	Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 +ℋ 𝐵))
Theorem	shsub2 29696	Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐵 +ℋ 𝐴))
Theorem	choc0 29697	The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
⊢ (⊥‘0ℋ) = ℋ
Theorem	choc1 29698	The orthocomplement of the unit subspace is the zero subspace. Does not require Axiom of Choice. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (⊥‘ ℋ) = 0ℋ
Theorem	chocnul 29699	Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.)
⊢ (⊥‘∅) = ℋ
Theorem	shintcli 29700	Closure of intersection of a nonempty subset of Sℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅)    ⇒   ⊢ ∩ 𝐴 ∈ Sℋ