HomeTheorem List (p. 313 of 500)
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. 313 of 500) | < 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-30909) |
Hilbert Space Explorer
(30910-32432) |
Users' Mathboxes
(32433-49920) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | shss 31201 | 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 31202 | 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 31203 | 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 31204 | 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 31205 | 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 31206 | 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 31207 | 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 31208 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻) | ||
| Theorem | shmulcl 31209 | 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 31210* | Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))) | ||
| Theorem | shsubcl 31211 | 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 31212 | 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 31213. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 31214 and isch3 31232. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
| ⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ} | ||
| Theorem | isch 31213 | 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 31214* | 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 31215 | 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 31216 | 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 31217 | 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 31218 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
| Theorem | ch0 31219 | 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 31220 | 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 31221 | 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 31222 | 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 31223 | 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 31224 | 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 31225 | 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 31226 | 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 31227 | 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 31228 | Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ | ||
| Theorem | hlimuni 31229 | 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 31230* | 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 31231* | 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 31232* | 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 31233* | Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥) | ||
| Theorem | helch 31234 | 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 31235 | Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.) |
| ⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ | ||
| Theorem | helsh 31236 | Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ ℋ ∈ Sℋ | ||
| Theorem | shsspwh 31237 | Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
| ⊢ Sℋ ⊆ 𝒫 ℋ | ||
| Theorem | chsspwh 31238 | Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
| ⊢ Cℋ ⊆ 𝒫 ℋ | ||
| Theorem | hsn0elch 31239 | 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 31240 | 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 31241* | 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 31242 | 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 31243* | 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 31271 and chocvali 31290 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 31244 | Define the zero for closed subspaces of Hilbert space. See h0elch 31246 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ 0ℋ = {0ℎ} | ||
| Theorem | elch0 31245 | Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ) | ||
| Theorem | h0elch 31246 | 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 31247 | The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ 0ℋ ∈ Sℋ | ||
| Theorem | hhssva 31248 | The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊) | ||
| Theorem | hhsssm 31249 | The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊) | ||
| Theorem | hhssnm 31250 | The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊) | ||
| Theorem | issubgoilem 31251* | Lemma for hhssabloilem 31252. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
| ⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦)) ⇒ ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵)) | ||
| Theorem | hhssabloilem 31252 | Lemma for hhssabloi 31253. Formerly part of proof for hhssabloi 31253 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 31253 | 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 31254 | Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp) | ||
| Theorem | hhssnv 31255 | Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝑊 ∈ NrmCVec | ||
| Theorem | hhssnvt 31256 | Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec) | ||
| Theorem | hhsst 31257 | A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈)) | ||
| Theorem | hhshsslem1 31258 | Lemma for hhsssh 31260. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
| Theorem | hhshsslem2 31259 | Lemma for hhsssh 31260. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
| Theorem | hhsssh 31260 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ)) | ||
| Theorem | hhsssh2 31261 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ)) | ||
| Theorem | hhssba 31262 | The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
| Theorem | hhssvs 31263 | The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊) | ||
| Theorem | hhssvsf 31264 | Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻 | ||
| Theorem | hhssims 31265 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐻 ∈ Sℋ & ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) ⇒ ⊢ 𝐷 = (IndMet‘𝑊) | ||
| Theorem | hhssims2 31266 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) | ||
| Theorem | hhssmet 31267 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩ & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 ∈ (Met‘𝐻) | ||
| Theorem | hhssmetdval 31268 | 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 31269 | 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 31270 | Obsolete version of cssbn 25312: 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 31271* | 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 31272* | Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
| Theorem | shocel 31273* | Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
| Theorem | ocsh 31274 | 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 31275 | 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 31276 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ⊆ ℋ) | ||
| Theorem | shocss 31277 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ⊆ ℋ) | ||
| Theorem | occon 31278 | Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘𝐵) ⊆ (⊥‘𝐴))) | ||
| Theorem | occon2 31279 | Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵)))) | ||
| Theorem | occon2i 31280 | Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵))) | ||
| Theorem | oc0 31281 | 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 31282 | Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | shocorth 31283 | Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | ococss 31284 | 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 31285 | 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 31286 | Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → (𝐺 ⊆ (⊥‘𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ih 𝐵) = 0))) | ||
| Theorem | ocin 31287 | 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 31288 | Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴))) | ||
| Theorem | ocnel 31289 | 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 31290* | 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 31291 | 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 31292 | 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 31293* | 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 31294 | Lemma for occl 31295. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℋ) & ⊢ (𝜑 → 𝐹 ∈ Cauchy) & ⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (( ⇝𝑣 ‘𝐹) ·ih 𝐵) = 0) | ||
| Theorem | occl 31295 | 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 31296 | 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 31297 | 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 31298 | Closure of Cℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) ∈ Cℋ | ||
| Definition | df-shs 31299* | Define subspace sum in Sℋ. See shsval 31303, shsval2i 31378, and shsval3i 31379 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
| ⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦))) | ||
| Definition | df-span 31300* | Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 31324 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ span = (𝑥 ∈ 𝒫 ℋ ↦ ∩ {𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |