P. 314 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31301-31400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	helch 31301	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 31302	Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.)
⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ
Theorem	helsh 31303	Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ℋ ∈ Sℋ
Theorem	shsspwh 31304	Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Sℋ ⊆ 𝒫 ℋ
Theorem	chsspwh 31305	Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.)
⊢ Cℋ ⊆ 𝒫 ℋ
Theorem	hsn0elch 31306	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 31307	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 31308*	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 31309	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 31310*	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 31338 and chocvali 31357 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 31311	Define the zero for closed subspaces of Hilbert space. See h0elch 31313 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ 0ℋ = {0ℎ}
Theorem	elch0 31312	Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.)
⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ)
Theorem	h0elch 31313	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 31314	The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ 0ℋ ∈ Sℋ
Theorem	hhssva 31315	The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊)
Theorem	hhsssm 31316	The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊)
Theorem	hhssnm 31317	The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊)
Theorem	issubgoilem 31318*	Lemma for hhssabloilem 31319. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵))
Theorem	hhssabloilem 31319	Lemma for hhssabloi 31320. Formerly part of proof for hhssabloi 31320 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 31320	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 31321	Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp)
Theorem	hhssnv 31322	Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝑊 ∈ NrmCVec
Theorem	hhssnvt 31323	Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec)
Theorem	hhsst 31324	A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈))
Theorem	hhshsslem1 31325	Lemma for hhsssh 31327. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhshsslem2 31326	Lemma for hhsssh 31327. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝑊 ∈ (SubSp‘𝑈)    &   ⊢ 𝐻 ⊆ ℋ    ⇒   ⊢ 𝐻 ∈ Sℋ
Theorem	hhsssh 31327	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ))
Theorem	hhsssh2 31328	The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    ⇒   ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ))
Theorem	hhssba 31329	The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐻 = (BaseSet‘𝑊)
Theorem	hhssvs 31330	The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊)
Theorem	hhssvsf 31331	Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻
Theorem	hhssims 31332	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))    ⇒   ⊢ 𝐷 = (IndMet‘𝑊)
Theorem	hhssims2 31333	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻))
Theorem	hhssmet 31334	Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ 𝐷 ∈ (Met‘𝐻)
Theorem	hhssmetdval 31335	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 31336	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 31337	Obsolete version of cssbn 25335: 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 31338*	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 31339*	Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	shocel 31340*	Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0)))
Theorem	ocsh 31341	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 31342	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 31343	An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ⊆ ℋ)
Theorem	shocss 31344	An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ⊆ ℋ)
Theorem	occon 31345	Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘𝐵) ⊆ (⊥‘𝐴)))
Theorem	occon2 31346	Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵))))
Theorem	occon2i 31347	Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ 𝐴 ⊆ ℋ    &   ⊢ 𝐵 ⊆ ℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵)))
Theorem	oc0 31348	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 31349	Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ (𝐻 ⊆ ℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0))
Theorem	shocorth 31350	Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0))
Theorem	ococss 31351	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 31352	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 31353	Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ (𝐻 ∈ Sℋ → (𝐺 ⊆ (⊥‘𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ih 𝐵) = 0)))
Theorem	ocin 31354	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 31355	Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴)))
Theorem	ocnel 31356	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 31357*	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 31358	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 31359	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 31360*	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 31361	Lemma for occl 31362. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ⊆ ℋ)    &   ⊢ (𝜑 → 𝐹 ∈ Cauchy)    &   ⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (( ⇝𝑣 ‘𝐹) ·ih 𝐵) = 0)
Theorem	occl 31362	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 31363	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 31364	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 31365	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 31366*	Define subspace sum in Sℋ. See shsval 31370, shsval2i 31445, and shsval3i 31446 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦)))
Definition	df-span 31367*	Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 31391 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ span = (𝑥 ∈ 𝒫 ℋ ↦ ∩ {𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦})
Definition	df-chj 31368*	Define Hilbert lattice join. See chjval 31410 for its value and chjcl 31415 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 31413. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦))))
Definition	df-chsup 31369	Define the supremum of a set of Hilbert lattice elements. See chsupval2 31468 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 31397. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.)
⊢ ∨ℋ = (𝑥 ∈ 𝒫 𝒫 ℋ ↦ (⊥‘(⊥‘∪ 𝑥)))
Theorem	shsval 31370	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 31371	The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ⊆ ℋ)
Theorem	shsel 31372*	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 31373*	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 31374*	Membership in subspace sum. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))
Theorem	shscli 31375	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 31376	Closure of subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ∈ Sℋ )
Theorem	shscom 31377	Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴))
Theorem	shsva 31378	Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsel1 31379	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 31380	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 31381	Vector subtraction belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)))
Theorem	shsub1 31382	Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 +ℋ 𝐵))
Theorem	shsub2 31383	Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐵 +ℋ 𝐴))
Theorem	choc0 31384	The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.)
⊢ (⊥‘0ℋ) = ℋ
Theorem	choc1 31385	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 31386	Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.)
⊢ (⊥‘∅) = ℋ
Theorem	shintcli 31387	Closure of intersection of a nonempty subset of Sℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅)    ⇒   ⊢ ∩ 𝐴 ∈ Sℋ
Theorem	shintcl 31388	The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Sℋ )
Theorem	chintcli 31389	The intersection of a nonempty set of closed subspaces is a closed subspace. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅)    ⇒   ⊢ ∩ 𝐴 ∈ Cℋ
Theorem	chintcl 31390	The intersection (infimum) of a nonempty subset of Cℋ belongs to Cℋ. Part of Theorem 3.13 of [Beran] p. 108. Also part of Definition 3.4-1 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Cℋ )
Theorem	spanval 31391*	Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in [Schechter] p. 276. (Contributed by NM, 2-Jun-2004.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) = ∩ {𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥})
Theorem	hsupval 31392	Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 31467. (Contributed by NM, 9-Dec-2003.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴)))
Theorem	chsupval 31393	The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 31468. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴)))
Theorem	spancl 31394	The span of a subset of Hilbert space is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) ∈ Sℋ )
Theorem	elspancl 31395	A member of a span is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ∈ (span‘𝐴)) → 𝐵 ∈ ℋ)
Theorem	shsupcl 31396	Closure of the subspace supremum of set of subsets of Hilbert space. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 ℋ → (span‘∪ 𝐴) ∈ Sℋ )
Theorem	hsupcl 31397	Closure of supremum of set of subsets of Hilbert space. Note that the supremum belongs to Cℋ even if the subsets do not. (Contributed by NM, 10-Nov-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) ∈ Cℋ )
Theorem	chsupcl 31398	Closure of supremum of subset of Cℋ. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. Shows that Cℋ is a complete lattice. Also part of Definition 3.4-1 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 10-Nov-1999.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) ∈ Cℋ )
Theorem	hsupss 31399	Subset relation for supremum of Hilbert space subsets. (Contributed by NM, 24-Nov-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵)))
Theorem	chsupss 31400	Subset relation for supremum of subset of Cℋ. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐵 ⊆ Cℋ ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵)))