| Metamath
Proof Explorer Theorem List (p. 313 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bcs2 31201 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 31199. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐵)) | ||
| Theorem | bcs3 31202 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 31199. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐵) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐴)) | ||
| Theorem | hcau 31203* | Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝑥)) | ||
| Theorem | hcauseq 31204 | A Cauchy sequences on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ (𝐹 ∈ Cauchy → 𝐹:ℕ⟶ ℋ) | ||
| Theorem | hcaucvg 31205* | A Cauchy sequence on a Hilbert space converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐹 ∈ Cauchy ∧ 𝐴 ∈ ℝ+) → ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝐴) | ||
| Theorem | seq1hcau 31206* | A sequence on a Hilbert space is a Cauchy sequence if it converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ (𝐹:ℕ⟶ ℋ → (𝐹 ∈ Cauchy ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝑥)) | ||
| Theorem | hlimi 31207* | Express the predicate: The limit of vector sequence 𝐹 in a Hilbert space is 𝐴, i.e. 𝐹 converges to 𝐴. This means that for any real 𝑥, no matter how small, there always exists an integer 𝑦 such that the norm of any later vector in the sequence minus the limit is less than 𝑥. Definition of converge in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹 ⇝𝑣 𝐴 ↔ ((𝐹:ℕ⟶ ℋ ∧ 𝐴 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑧) −ℎ 𝐴)) < 𝑥)) | ||
| Theorem | hlimseqi 31208 | A sequence with a limit on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐹:ℕ⟶ ℋ) | ||
| Theorem | hlimveci 31209 | Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ) | ||
| Theorem | hlimconvi 31210* | Convergence of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ((𝐹 ⇝𝑣 𝐴 ∧ 𝐵 ∈ ℝ+) → ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑧) −ℎ 𝐴)) < 𝐵) | ||
| Theorem | hlim2 31211* | The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐹:ℕ⟶ ℋ ∧ 𝐴 ∈ ℋ) → (𝐹 ⇝𝑣 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑧) −ℎ 𝐴)) < 𝑥)) | ||
| Theorem | hlimadd 31212* | Limit of the sum of two sequences in a Hilbert vector space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶ ℋ) & ⊢ (𝜑 → 𝐺:ℕ⟶ ℋ) & ⊢ (𝜑 → 𝐹 ⇝𝑣 𝐴) & ⊢ (𝜑 → 𝐺 ⇝𝑣 𝐵) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛) +ℎ (𝐺‘𝑛))) ⇒ ⊢ (𝜑 → 𝐻 ⇝𝑣 (𝐴 +ℎ 𝐵)) | ||
| Theorem | hilmet 31213 | The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (Met‘ ℋ) | ||
| Theorem | hilxmet 31214 | The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (∞Met‘ ℋ) | ||
| Theorem | hilmetdval 31215 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵))) | ||
| Theorem | hilims 31216 | Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.) |
| ⊢ ℋ = (BaseSet‘𝑈) & ⊢ +ℎ = ( +𝑣 ‘𝑈) & ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) & ⊢ ·ih = (·𝑖OLD‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ 𝐷 = (normℎ ∘ −ℎ ) | ||
| Theorem | hhcau 31217 | The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑m ℕ)) | ||
| Theorem | hhlm 31218 | The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑m ℕ)) | ||
| Theorem | hhcmpl 31219* | Lemma used for derivation of the completeness axiom ax-hcompl 31221 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥) ⇒ ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
| Theorem | hilcompl 31220* | Lemma used for derivation of the completeness axiom ax-hcompl 31221 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 31018; the 6th would be satisfied by eqid 2737; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl 30934. (Contributed by NM, 13-Sep-2007.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ ℋ = (BaseSet‘𝑈) & ⊢ +ℎ = ( +𝑣 ‘𝑈) & ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) & ⊢ ·ih = (·𝑖OLD‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑈 ∈ CHilOLD & ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥) ⇒ ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
| Axiom | ax-hcompl 31221* | Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
| Theorem | hhcms 31222 | The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008.) (Proof shortened by Mario Carneiro, 14-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (CMet‘ ℋ) | ||
| Theorem | hhhl 31223 | The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ 𝑈 ∈ CHilOLD | ||
| Theorem | hilcms 31224 | The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (CMet‘ ℋ) | ||
| Theorem | hilhl 31225 | The Hilbert space of the Hilbert Space Explorer is a complex Hilbert space. (Contributed by Steve Rodriguez, 29-Apr-2007.) (New usage is discouraged.) |
| ⊢ 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ∈ CHilOLD | ||
| Definition | df-sh 31226 | Define the set of subspaces of a Hilbert space. See issh 31227 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ Sℋ = {ℎ ∈ 𝒫 ℋ ∣ (0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ “ (ℂ × ℎ)) ⊆ ℎ)} | ||
| Theorem | issh 31227 | Subspace 𝐻 of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻))) | ||
| Theorem | issh2 31228* | Subspace 𝐻 of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻))) | ||
| Theorem | shss 31229 | 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 31230 | 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 31231 | 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 31232 | 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 31233 | 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 31234 | 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 31235 | 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 31236 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻) | ||
| Theorem | shmulcl 31237 | 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 31238* | Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))) | ||
| Theorem | shsubcl 31239 | 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 31240 | 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 31241. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 31242 and isch3 31260. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
| ⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ} | ||
| Theorem | isch 31241 | 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 31242* | 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 31243 | 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 31244 | 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 31245 | 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 31246 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
| Theorem | ch0 31247 | 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 31248 | 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 31249 | 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 31250 | 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 31251 | 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 31252 | 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 31253 | 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 31254 | 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 31255 | 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 31256 | Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
| ⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ | ||
| Theorem | hlimuni 31257 | 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 31258* | 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 31259* | 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 31260* | 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 31261* | Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥) | ||
| Theorem | helch 31262 | 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 31263 | Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.) |
| ⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ | ||
| Theorem | helsh 31264 | Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ ℋ ∈ Sℋ | ||
| Theorem | shsspwh 31265 | Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
| ⊢ Sℋ ⊆ 𝒫 ℋ | ||
| Theorem | chsspwh 31266 | Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
| ⊢ Cℋ ⊆ 𝒫 ℋ | ||
| Theorem | hsn0elch 31267 | 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 31268 | 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 31269* | 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 31270 | 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 31271* | 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 31299 and chocvali 31318 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 31272 | Define the zero for closed subspaces of Hilbert space. See h0elch 31274 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ 0ℋ = {0ℎ} | ||
| Theorem | elch0 31273 | Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ) | ||
| Theorem | h0elch 31274 | 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 31275 | The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ 0ℋ ∈ Sℋ | ||
| Theorem | hhssva 31276 | The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊) | ||
| Theorem | hhsssm 31277 | The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊) | ||
| Theorem | hhssnm 31278 | The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊) | ||
| Theorem | issubgoilem 31279* | Lemma for hhssabloilem 31280. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
| ⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦)) ⇒ ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵)) | ||
| Theorem | hhssabloilem 31280 | Lemma for hhssabloi 31281. Formerly part of proof for hhssabloi 31281 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 31281 | 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 31282 | Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp) | ||
| Theorem | hhssnv 31283 | Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝑊 ∈ NrmCVec | ||
| Theorem | hhssnvt 31284 | Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec) | ||
| Theorem | hhsst 31285 | A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈)) | ||
| Theorem | hhshsslem1 31286 | Lemma for hhsssh 31288. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
| Theorem | hhshsslem2 31287 | Lemma for hhsssh 31288. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
| Theorem | hhsssh 31288 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ)) | ||
| Theorem | hhsssh2 31289 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ)) | ||
| Theorem | hhssba 31290 | The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
| Theorem | hhssvs 31291 | The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊) | ||
| Theorem | hhssvsf 31292 | Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻 | ||
| Theorem | hhssims 31293 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ & ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) ⇒ ⊢ 𝐷 = (IndMet‘𝑊) | ||
| Theorem | hhssims2 31294 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) | ||
| Theorem | hhssmet 31295 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 ∈ (Met‘𝐻) | ||
| Theorem | hhssmetdval 31296 | 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 31297 | 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 31298 | Obsolete version of cssbn 25409: 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 31299* | 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 31300* | Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |