Home | Metamath
Proof Explorer Theorem List (p. 275 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hilablo 27401 | Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
⊢ +ℎ ∈ AbelOp | ||
Theorem | hilid 27402 | The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007.) (New usage is discouraged.) |
⊢ (GId‘ +ℎ ) = 0ℎ | ||
Theorem | hilvc 27403 | Hilbert space is a complex vector space. Vector addition is +ℎ, and scalar product is ·ℎ. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
⊢ 〈 +ℎ , ·ℎ 〉 ∈ CVecOLD | ||
Theorem | hilnormi 27404 | Hilbert space norm in terms of vector space norm. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ℋ = (BaseSet‘𝑈) & ⊢ ·ih = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
Theorem | hilhhi 27405 | Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ ℋ = (BaseSet‘𝑈) & ⊢ +ℎ = ( +𝑣 ‘𝑈) & ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) & ⊢ ·ih = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 | ||
Theorem | hhnv 27406 | Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
Theorem | hhva 27407 | The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
Theorem | hhba 27408 | The base set of Hilbert space. This theorem provides an independent proof of df-hba 27210 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ ℋ = (BaseSet‘𝑈) | ||
Theorem | hh0v 27409 | The zero vector of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ 0ℎ = (0vec‘𝑈) | ||
Theorem | hhsm 27410 | The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
Theorem | hhvs 27411 | The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ −ℎ = ( −𝑣 ‘𝑈) | ||
Theorem | hhnm 27412 | The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
Theorem | hhims 27413 | The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 = (IndMet‘𝑈) | ||
Theorem | hhims2 27414 | Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 = (normℎ ∘ −ℎ ) | ||
Theorem | hhmet 27415 | The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (Met‘ ℋ) | ||
Theorem | hhxmet 27416 | The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (∞Met‘ ℋ) | ||
Theorem | hhmetdval 27417 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵))) | ||
Theorem | hhip 27418 | The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ ·ih = (·𝑖OLD‘𝑈) | ||
Theorem | hhph 27419 | The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ 𝑈 ∈ CPreHilOLD | ||
Theorem | bcsiALT 27420 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵)) | ||
Theorem | bcsiHIL 27421 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Proved from ZFC version.) (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵)) | ||
Theorem | bcs 27422 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵))) | ||
Theorem | bcs2 27423 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 27421. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐵)) | ||
Theorem | bcs3 27424 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 27421. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐵) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐴)) | ||
Theorem | hcau 27425* | 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 27426 | 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 27427* | 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 27428* | 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 27429* | 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 27430 | 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 27431 | Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ) | ||
Theorem | hlimconvi 27432* | 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 27433* | 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 27434* | 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 27435 | The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (Met‘ ℋ) | ||
Theorem | hilxmet 27436 | The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (∞Met‘ ℋ) | ||
Theorem | hilmetdval 27437 | 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 27438 | Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.) |
⊢ ℋ = (BaseSet‘𝑈) & ⊢ +ℎ = ( +𝑣 ‘𝑈) & ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) & ⊢ ·ih = (·𝑖OLD‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ 𝐷 = (normℎ ∘ −ℎ ) | ||
Theorem | hhcau 27439 | The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑𝑚 ℕ)) | ||
Theorem | hhlm 27440 | The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑𝑚 ℕ)) | ||
Theorem | hhcmpl 27441* | Lemma used for derivation of the completeness axiom ax-hcompl 27443 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥) ⇒ ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
Theorem | hilcompl 27442* | Lemma used for derivation of the completeness axiom ax-hcompl 27443 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 27240; the 6th would be satisfied by eqid 2610; the 7th by a given fixed Hilbert space; and the last by theorem hlcompl 27155. (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 27443* | Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
Theorem | hhcms 27444 | The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (CMet‘ ℋ) | ||
Theorem | hhhl 27445 | The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ 𝑈 ∈ CHilOLD | ||
Theorem | hilcms 27446 | The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (CMet‘ ℋ) | ||
Theorem | hilhl 27447 | 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 27448 | Define the set of subspaces of a Hilbert space. See issh 27449 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 27449 | 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 27450* | 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 27451 | 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 27452 | 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 27453 | 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 27454 | 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 27455 | 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 27456 | 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 27457 | 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 27458 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻) | ||
Theorem | shmulcl 27459 | 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 27460* | Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))) | ||
Theorem | shsubcl 27461 | 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 27462 | 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 27463. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 27464 and isch3 27482. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑𝑚 ℕ)) ⊆ ℎ} | ||
Theorem | isch 27463 | 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 27464* | 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 27465 | 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 27466 | 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 27467 | 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 27468 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
Theorem | ch0 27469 | 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 27470 | 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 27471 | 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 27472 | 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 27473 | 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 27474 | 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 27475 | 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 27476 | 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 27477 | 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 27478 | Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ | ||
Theorem | hlimuni 27479 | 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 27480* | 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 27481* | 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 27482* | 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 27483* | Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹:ℕ⟶𝐻) → ∃𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥) | ||
Theorem | helch 27484 | 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 27485 | Prove if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.) |
⊢ if(𝐴 ∈ Cℋ , 𝐴, ℋ) ∈ Cℋ | ||
Theorem | helsh 27486 | Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ ℋ ∈ Sℋ | ||
Theorem | shsspwh 27487 | Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
⊢ Sℋ ⊆ 𝒫 ℋ | ||
Theorem | chsspwh 27488 | Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
⊢ Cℋ ⊆ 𝒫 ℋ | ||
Theorem | hsn0elch 27489 | 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 27490 | 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 27491* | 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 27492 | 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 27493* | 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 27523 and chocvali 27542 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 27494 | Define the zero for closed subspaces of Hilbert space. See h0elch 27496 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ 0ℋ = {0ℎ} | ||
Theorem | elch0 27495 | Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ) | ||
Theorem | h0elch 27496 | 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 27497 | The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ 0ℋ ∈ Sℋ | ||
Theorem | hhssva 27498 | The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) = ( +𝑣 ‘𝑊) | ||
Theorem | hhsssm 27499 | The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) = ( ·𝑠OLD ‘𝑊) | ||
Theorem | hhssnm 27500 | The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (normℎ ↾ 𝐻) = (normCV‘𝑊) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |