P. 313 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31201-31300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chssii 31201	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 31202	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 31203	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 31204	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 31205	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 31206	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 31207	Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
Theorem	hlimuni 31208	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 31209*	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 31210*	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 31211*	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 31212*	Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥)
Theorem	helch 31213	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 31214	Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.)
⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ
Theorem	helsh 31215	Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ℋ ∈ Sℋ
Theorem	shsspwh 31216	Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Sℋ ⊆ 𝒫 ℋ
Theorem	chsspwh 31217	Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Cℋ ⊆ 𝒫 ℋ
Theorem	hsn0elch 31218	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 31219	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 31220*	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 31221	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 31222*	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 31250 and chocvali 31269 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 31223	Define the zero for closed subspaces of Hilbert space. See h0elch 31225 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ 0ℋ = {0ℎ}
Theorem	elch0 31224	Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.)
⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ)
Theorem	h0elch 31225	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 31226	The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ 0ℋ ∈ Sℋ
Theorem	hhssva 31227	The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊)
Theorem	hhsssm 31228	The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊)
Theorem	hhssnm 31229	The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊)
Theorem	issubgoilem 31230*	Lemma for hhssabloilem 31231. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵))
Theorem	hhssabloilem 31231	Lemma for hhssabloi 31232. Formerly part of proof for hhssabloi 31232 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 31232	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 31233	Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp)
Theorem	hhssnv 31234	Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝑊 ∈ NrmCVec
Theorem	hhssnvt 31235	Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec)
Theorem	hhsst 31236	A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈))
Theorem	hhshsslem1 31237	Lemma for hhsssh 31239. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhshsslem2 31238	Lemma for hhsssh 31239. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 ∈ Sℋ
Theorem	hhsssh 31239	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ))
Theorem	hhsssh2 31240	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ))
Theorem	hhssba 31241	The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhssvs 31242	The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊)
Theorem	hhssvsf 31243	Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻
Theorem	hhssims 31244	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))    ⇒   ⊢ 𝐷 = (IndMet‘𝑊)
Theorem	hhssims2 31245	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))
Theorem	hhssmet 31246	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 ∈ (Met‘𝐻)
Theorem	hhssmetdval 31247	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 31248	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 31249	Obsolete version of cssbn 25295: 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 31250*	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 31251*	Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	shocel 31252*	Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	ocsh 31253	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 31254	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 31255	An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ⊆ ℋ)
Theorem	shocss 31256	An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ⊆ ℋ)
Theorem	occon 31257	Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘𝐵) ⊆ (⊥‘𝐴)))
Theorem	occon2 31258	Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵))))
Theorem	occon2i 31259	Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ 𝐴 ⊆ ℋ    &   ⊢ 𝐵 ⊆ ℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵)))
Theorem	oc0 31260	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 31261	Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0))
Theorem	shocorth 31262	Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0))
Theorem	ococss 31263	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 31264	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 31265	Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → (𝐺 ⊆ (⊥‘𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ih 𝐵) = 0)))
Theorem	ocin 31266	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 31267	Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴)))
Theorem	ocnel 31268	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 31269*	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 31270	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 31271	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 31272*	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 31273	Lemma for occl 31274. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ⊆ ℋ)    &   ⊢ (𝜑 → 𝐹 ∈ Cauchy)    &   ⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (( ⇝𝑣 ‘𝐹) ·ih 𝐵) = 0)
Theorem	occl 31274	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 31275	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 31276	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 31277	Closure of Cℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) ∈ Cℋ
20.4.4  Subspace sum, span, lattice join, lattice supremum
Definition	df-shs 31278*	Define subspace sum in Sℋ. See shsval 31282, shsval2i 31357, and shsval3i 31358 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦)))
Definition	df-span 31279*	Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 31303 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ span = (𝑥 ∈ 𝒫 ℋ ↦ ∩ {𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦})
Definition	df-chj 31280*	Define Hilbert lattice join. See chjval 31322 for its value and chjcl 31327 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 31325. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦))))
Definition	df-chsup 31281	Define the supremum of a set of Hilbert lattice elements. See chsupval2 31380 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 31309. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.)
⊢ ∨ℋ = (𝑥 ∈ 𝒫 𝒫 ℋ ↦ (⊥‘(⊥‘∪ 𝑥)))
Theorem	shsval 31282	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 31283	The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ⊆ ℋ)
Theorem	shsel 31284*	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 31285*	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 31286*	Membership in subspace sum. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))
Theorem	shscli 31287	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 31288	Closure of subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ∈ Sℋ )
Theorem	shscom 31289	Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴))
Theorem	shsva 31290	Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsel1 31291	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 31292	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 31293	Vector subtraction belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsub1 31294	Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 +ℋ 𝐵))
Theorem	shsub2 31295	Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐵 +ℋ 𝐴))
Theorem	choc0 31296	The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
⊢ (⊥‘0ℋ) = ℋ
Theorem	choc1 31297	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 31298	Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.)
⊢ (⊥‘∅) = ℋ
Theorem	shintcli 31299	Closure of intersection of a nonempty subset of Sℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅)    ⇒   ⊢ ∩ 𝐴 ∈ Sℋ
Theorem	shintcl 31300	The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Sℋ )