HomeTheorem List (p. 283 of 429)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 283 of 429) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27903) |
Hilbert Space Explorer
(27904-29428) |
Users' Mathboxes
(29429-42879) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sh0 28201 | 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 28202 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻) | ||
| Theorem | shmulcl 28203 | 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 28204* | Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))) | ||
| Theorem | shsubcl 28205 | Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 −ℎ 𝐵) ∈ 𝐻) | ||
| Definition | df-ch 28206 | 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 28207. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 28208 and isch3 28226. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
| ⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑𝑚 ℕ)) ⊆ ℎ} | ||
| Theorem | isch 28207 | 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ℋ ∧ ( ⇝𝑣 “ (𝐻 ↑𝑚 ℕ)) ⊆ 𝐻)) | ||
| Theorem | isch2 28208* | 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 28209 | 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 28210 | 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 28211 | 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 28212 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
| Theorem | ch0 28213 | 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 28214 | 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 28215 | 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 28216 | 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 28217 | 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 28218 | 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 28219 | 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 28220 | 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 28221 | 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 28222 | Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ | ||
| Theorem | hlimuni 28223 | 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 28224* | 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 28225* | 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 28226* | 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 28227* | Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥) | ||
| Theorem | helch 28228 | 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 28229 | Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.) |
| ⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ | ||
| Theorem | helsh 28230 | Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ ℋ ∈ Sℋ | ||
| Theorem | shsspwh 28231 | Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
| ⊢ Sℋ ⊆ 𝒫 ℋ | ||
| Theorem | chsspwh 28232 | Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
| ⊢ Cℋ ⊆ 𝒫 ℋ | ||
| Theorem | hsn0elch 28233 | 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 28234 | 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 28235* | 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 28236 | 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) | ||
| Definition | df-oc 28237* | 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 28267 and chocvali 28286 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 28238 | Define the zero for closed subspaces of Hilbert space. See h0elch 28240 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ 0ℋ = {0ℎ} | ||
| Theorem | elch0 28239 | Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ) | ||
| Theorem | h0elch 28240 | 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 28241 | The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ 0ℋ ∈ Sℋ | ||
| Theorem | hhssva 28242 | The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊) | ||
| Theorem | hhsssm 28243 | The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊) | ||
| Theorem | hhssnm 28244 | The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊) | ||
| Theorem | issubgoilem 28245* | Lemma for hhssabloilem 28246. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
| ⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦)) ⇒ ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵)) | ||
| Theorem | hhssabloilem 28246 | Lemma for hhssabloi 28247. Formerly part of proof for hhssabloi 28247 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 28247 | 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 28248 | Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp) | ||
| Theorem | hhssnv 28249 | Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝑊 ∈ NrmCVec | ||
| Theorem | hhssnvt 28250 | Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec) | ||
| Theorem | hhsst 28251 | A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈)) | ||
| Theorem | hhshsslem1 28252 | Lemma for hhsssh 28254. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
| Theorem | hhshsslem2 28253 | Lemma for hhsssh 28254. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
| Theorem | hhsssh 28254 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ)) | ||
| Theorem | hhsssh2 28255 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ)) | ||
| Theorem | hhssba 28256 | The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
| Theorem | hhssvs 28257 | The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊) | ||
| Theorem | hhssvsf 28258 | Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻 | ||
| Theorem | hhssph 28259 | Inner product space property of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝑊 ∈ CPreHilOLD | ||
| Theorem | hhssims 28260 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ & ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) ⇒ ⊢ 𝐷 = (IndMet‘𝑊) | ||
| Theorem | hhssims2 28261 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) | ||
| Theorem | hhssmet 28262 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 ∈ (Met‘𝐻) | ||
| Theorem | hhssmetdval 28263 | 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 28264 | 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 | hhssbn 28265 | Banach space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝑊 ∈ CBan | ||
| Theorem | hhsshl 28266 | Hilbert space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝑊 ∈ CHilOLD | ||
| Theorem | ocval 28267* | 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 28268* | Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
| Theorem | shocel 28269* | Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
| Theorem | ocsh 28270 | 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 28271 | 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 28272 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ⊆ ℋ) | ||
| Theorem | shocss 28273 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ⊆ ℋ) | ||
| Theorem | occon 28274 | Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘𝐵) ⊆ (⊥‘𝐴))) | ||
| Theorem | occon2 28275 | Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵)))) | ||
| Theorem | occon2i 28276 | Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵))) | ||
| Theorem | oc0 28277 | 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 28278 | Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | shocorth 28279 | Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | ococss 28280 | 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 28281 | 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 28282 | Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → (𝐺 ⊆ (⊥‘𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ih 𝐵) = 0))) | ||
| Theorem | ocin 28283 | 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 28284 | Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴))) | ||
| Theorem | ocnel 28285 | 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 28286* | 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 28287 | 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 28288 | 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 28289* | 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 28290 | Lemma for occl 28291. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℋ) & ⊢ (𝜑 → 𝐹 ∈ Cauchy) & ⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (( ⇝𝑣 ‘𝐹) ·ih 𝐵) = 0) | ||
| Theorem | occl 28291 | 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 28292 | 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 28293 | 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 28294 | Closure of Cℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) ∈ Cℋ | ||
| Definition | df-shs 28295* | Define subspace sum in Sℋ. See shsval 28299, shsval2i 28374, and shsval3i 28375 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
| ⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦))) | ||
| Definition | df-span 28296* | Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 28320 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ span = (𝑥 ∈ 𝒫 ℋ ↦ ∩ {𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦}) | ||
| Definition | df-chj 28297* | Define Hilbert lattice join. See chjval 28339 for its value and chjcl 28344 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 28342. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
| ⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) | ||
| Definition | df-chsup 28298 | Define the supremum of a set of Hilbert lattice elements. See chsupval2 28397 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 28326. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.) |
| ⊢ ∨ℋ = (𝑥 ∈ 𝒫 𝒫 ℋ ↦ (⊥‘(⊥‘∪ 𝑥))) | ||
| Theorem | shsval 28299 | 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 28300 | The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ⊆ ℋ) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |