HomeTheorem List (p. 312 of 497)
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. 312 of 497) | < 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-30899) |
Hilbert Space Explorer
(30900-32422) |
Users' Mathboxes
(32423-49669) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bcseqi 31101 | Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 31161. (Contributed by NM, 16-Jul-2001.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (((𝐴 ·ih 𝐵) · (𝐵 ·ih 𝐴)) = ((𝐴 ·ih 𝐴) · (𝐵 ·ih 𝐵)) ↔ ((𝐵 ·ih 𝐵) ·ℎ 𝐴) = ((𝐴 ·ih 𝐵) ·ℎ 𝐵)) | ||
| Theorem | normlem9at 31102 | Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 10-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) ·ih (𝐴 −ℎ 𝐵)) = (((𝐴 ·ih 𝐴) + (𝐵 ·ih 𝐵)) − ((𝐴 ·ih 𝐵) + (𝐵 ·ih 𝐴)))) | ||
| Theorem | dfhnorm2 31103 | Alternate definition of the norm of a vector of Hilbert space. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ normℎ = (𝑥 ∈ ℋ ↦ (√‘(𝑥 ·ih 𝑥))) | ||
| Theorem | normf 31104 | The norm function maps from Hilbert space to reals. (Contributed by NM, 6-Sep-2007.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ normℎ: ℋ⟶ℝ | ||
| Theorem | normval 31105 | The value of the norm of a vector in Hilbert space. Definition of norm in [Beran] p. 96. In the literature, the norm of 𝐴 is usually written as "|| 𝐴 ||", but we use function value notation to take advantage of our existing theorems about functions. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normℎ‘𝐴) = (√‘(𝐴 ·ih 𝐴))) | ||
| Theorem | normcl 31106 | Real closure of the norm of a vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normℎ‘𝐴) ∈ ℝ) | ||
| Theorem | normge0 31107 | The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → 0 ≤ (normℎ‘𝐴)) | ||
| Theorem | normgt0 31108 | The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 ≠ 0ℎ ↔ 0 < (normℎ‘𝐴))) | ||
| Theorem | norm0 31109 | The norm of a zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ (normℎ‘0ℎ) = 0 | ||
| Theorem | norm-i 31110 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ)) | ||
| Theorem | normne0 31111 | A norm is nonzero iff its argument is a nonzero vector. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) ≠ 0 ↔ 𝐴 ≠ 0ℎ)) | ||
| Theorem | normcli 31112 | Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (normℎ‘𝐴) ∈ ℝ | ||
| Theorem | normsqi 31113 | The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴) | ||
| Theorem | norm-i-i 31114 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 5-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ) | ||
| Theorem | normsq 31115 | The square of a norm. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴)) | ||
| Theorem | normsub0i 31116 | Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((normℎ‘(𝐴 −ℎ 𝐵)) = 0 ↔ 𝐴 = 𝐵) | ||
| Theorem | normsub0 31117 | Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((normℎ‘(𝐴 −ℎ 𝐵)) = 0 ↔ 𝐴 = 𝐵)) | ||
| Theorem | norm-ii-i 31118 | Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (normℎ‘(𝐴 +ℎ 𝐵)) ≤ ((normℎ‘𝐴) + (normℎ‘𝐵)) | ||
| Theorem | norm-ii 31119 | Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 +ℎ 𝐵)) ≤ ((normℎ‘𝐴) + (normℎ‘𝐵))) | ||
| Theorem | norm-iii-i 31120 | Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵)) | ||
| Theorem | norm-iii 31121 | Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵))) | ||
| Theorem | normsubi 31122 | Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (normℎ‘(𝐴 −ℎ 𝐵)) = (normℎ‘(𝐵 −ℎ 𝐴)) | ||
| Theorem | normpythi 31123 | Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 ·ih 𝐵) = 0 → ((normℎ‘(𝐴 +ℎ 𝐵))↑2) = (((normℎ‘𝐴)↑2) + ((normℎ‘𝐵)↑2))) | ||
| Theorem | normsub 31124 | Swapping order of subtraction doesn't change the norm of a vector. (Contributed by NM, 14-Aug-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) = (normℎ‘(𝐵 −ℎ 𝐴))) | ||
| Theorem | normneg 31125 | The norm of a vector equals the norm of its negative. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normℎ‘(-1 ·ℎ 𝐴)) = (normℎ‘𝐴)) | ||
| Theorem | normpyth 31126 | Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 → ((normℎ‘(𝐴 +ℎ 𝐵))↑2) = (((normℎ‘𝐴)↑2) + ((normℎ‘𝐵)↑2)))) | ||
| Theorem | normpyc 31127 | Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 → (normℎ‘𝐴) ≤ (normℎ‘(𝐴 +ℎ 𝐵)))) | ||
| Theorem | norm3difi 31128 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐴 −ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ 𝐵))) | ||
| Theorem | norm3adifii 31129 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (abs‘((normℎ‘(𝐴 −ℎ 𝐶)) − (normℎ‘(𝐵 −ℎ 𝐶)))) ≤ (normℎ‘(𝐴 −ℎ 𝐵)) | ||
| Theorem | norm3lem 31130 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ (((normℎ‘(𝐴 −ℎ 𝐶)) < (𝐷 / 2) ∧ (normℎ‘(𝐶 −ℎ 𝐵)) < (𝐷 / 2)) → (normℎ‘(𝐴 −ℎ 𝐵)) < 𝐷) | ||
| Theorem | norm3dif 31131 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 20-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐴 −ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ 𝐵)))) | ||
| Theorem | norm3dif2 31132 | Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐶 −ℎ 𝐴)) + (normℎ‘(𝐶 −ℎ 𝐵)))) | ||
| Theorem | norm3lemt 31133 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℝ)) → (((normℎ‘(𝐴 −ℎ 𝐶)) < (𝐷 / 2) ∧ (normℎ‘(𝐶 −ℎ 𝐵)) < (𝐷 / 2)) → (normℎ‘(𝐴 −ℎ 𝐵)) < 𝐷)) | ||
| Theorem | norm3adifi 31134 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 3-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘((normℎ‘(𝐴 −ℎ 𝐶)) − (normℎ‘(𝐵 −ℎ 𝐶)))) ≤ (normℎ‘(𝐴 −ℎ 𝐵))) | ||
| Theorem | normpari 31135 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (((normℎ‘(𝐴 −ℎ 𝐵))↑2) + ((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 · ((normℎ‘𝐴)↑2)) + (2 · ((normℎ‘𝐵)↑2))) | ||
| Theorem | normpar 31136 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((normℎ‘(𝐴 −ℎ 𝐵))↑2) + ((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 · ((normℎ‘𝐴)↑2)) + (2 · ((normℎ‘𝐵)↑2)))) | ||
| Theorem | normpar2i 31137 | Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100. (Contributed by NM, 5-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((normℎ‘(𝐴 −ℎ 𝐵))↑2) = (((2 · ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (2 · ((normℎ‘(𝐵 −ℎ 𝐶))↑2))) − ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2 ·ℎ 𝐶)))↑2)) | ||
| Theorem | polid2i 31138 | Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ (𝐴 ·ih 𝐵) = (((((𝐴 +ℎ 𝐶) ·ih (𝐷 +ℎ 𝐵)) − ((𝐴 −ℎ 𝐶) ·ih (𝐷 −ℎ 𝐵))) + (i · (((𝐴 +ℎ (i ·ℎ 𝐶)) ·ih (𝐷 +ℎ (i ·ℎ 𝐵))) − ((𝐴 −ℎ (i ·ℎ 𝐶)) ·ih (𝐷 −ℎ (i ·ℎ 𝐵)))))) / 4) | ||
| Theorem | polidi 31139 | Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 31065. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ih 𝐵) = (((((normℎ‘(𝐴 +ℎ 𝐵))↑2) − ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i · (((normℎ‘(𝐴 +ℎ (i ·ℎ 𝐵)))↑2) − ((normℎ‘(𝐴 −ℎ (i ·ℎ 𝐵)))↑2)))) / 4) | ||
| Theorem | polid 31140 | Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 31065. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (((((normℎ‘(𝐴 +ℎ 𝐵))↑2) − ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i · (((normℎ‘(𝐴 +ℎ (i ·ℎ 𝐵)))↑2) − ((normℎ‘(𝐴 −ℎ (i ·ℎ 𝐵)))↑2)))) / 4)) | ||
| Theorem | hilablo 31141 | Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
| ⊢ +ℎ ∈ AbelOp | ||
| Theorem | hilid 31142 | 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 31143 | 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 31144 | 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 31145 | 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 31146 | Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
| Theorem | hhva 31147 | The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
| Theorem | hhba 31148 | The base set of Hilbert space. This theorem provides an independent proof of df-hba 30950 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ⇒ ⊢ ℋ = (BaseSet‘𝑈) | ||
| Theorem | hh0v 31149 | 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 31150 | The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
| Theorem | hhvs 31151 | The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ⇒ ⊢ −ℎ = ( −𝑣 ‘𝑈) | ||
| Theorem | hhnm 31152 | The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
| Theorem | hhims 31153 | The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 = (IndMet‘𝑈) | ||
| Theorem | hhims2 31154 | Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 = (normℎ ∘ −ℎ ) | ||
| Theorem | hhmet 31155 | The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (Met‘ ℋ) | ||
| Theorem | hhxmet 31156 | The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (∞Met‘ ℋ) | ||
| Theorem | hhmetdval 31157 | 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 31158 | 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 31159 | 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 31160 | 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 31161 | 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 31162 | 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 31163 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 31161. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐵)) | ||
| Theorem | bcs3 31164 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 31161. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐵) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐴)) | ||
| Theorem | hcau 31165* | 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 31166 | 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 31167* | 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 31168* | 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 31169* | 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 31170 | 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 31171 | Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ) | ||
| Theorem | hlimconvi 31172* | 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 31173* | 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 31174* | 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 31175 | The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (Met‘ ℋ) | ||
| Theorem | hilxmet 31176 | The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (∞Met‘ ℋ) | ||
| Theorem | hilmetdval 31177 | 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 31178 | Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.) |
| ⊢ ℋ = (BaseSet‘𝑈) & ⊢ +ℎ = ( +𝑣 ‘𝑈) & ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) & ⊢ ·ih = (·𝑖OLD‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ 𝐷 = (normℎ ∘ −ℎ ) | ||
| Theorem | hhcau 31179 | The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑m ℕ)) | ||
| Theorem | hhlm 31180 | The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑m ℕ)) | ||
| Theorem | hhcmpl 31181* | Lemma used for derivation of the completeness axiom ax-hcompl 31183 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥) ⇒ ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
| Theorem | hilcompl 31182* | Lemma used for derivation of the completeness axiom ax-hcompl 31183 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 30980; the 6th would be satisfied by eqid 2735; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl 30896. (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 31183* | Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
| ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
| Theorem | hhcms 31184 | 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 31185 | The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ⇒ ⊢ 𝑈 ∈ CHilOLD | ||
| Theorem | hilcms 31186 | The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (CMet‘ ℋ) | ||
| Theorem | hilhl 31187 | 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 31188 | Define the set of subspaces of a Hilbert space. See issh 31189 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 31189 | 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 31190* | 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 31191 | 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 31192 | 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 31193 | 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 31194 | 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 31195 | 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 31196 | 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 31197 | 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 31198 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴 +ℎ 𝐵) ∈ 𝐻) | ||
| Theorem | shmulcl 31199 | 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 31200* | Subspace 𝐻 of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ (𝐻 ⊆ ℋ → (𝐻 ∈ Sℋ ↔ (0ℎ ∈ 𝐻 ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |