Home | Metamath
Proof Explorer Theorem List (p. 289 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hi01 28801 | Inner product with the 0 vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0ℎ ·ih 𝐴) = 0) | ||
Theorem | hi02 28802 | Inner product with the 0 vector. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 0ℎ) = 0) | ||
Theorem | hiidge0 28803 | Inner product with self is not negative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·ih 𝐴)) | ||
Theorem | his6 28804 | Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → ((𝐴 ·ih 𝐴) = 0 ↔ 𝐴 = 0ℎ)) | ||
Theorem | his1i 28805 | Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. (Contributed by NM, 15-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴)) | ||
Theorem | abshicom 28806 | Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) = (abs‘(𝐵 ·ih 𝐴))) | ||
Theorem | hial0 28807* | A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (∀𝑥 ∈ ℋ (𝐴 ·ih 𝑥) = 0 ↔ 𝐴 = 0ℎ)) | ||
Theorem | hial02 28808* | A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (∀𝑥 ∈ ℋ (𝑥 ·ih 𝐴) = 0 ↔ 𝐴 = 0ℎ)) | ||
Theorem | hisubcomi 28809 | Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = ((𝐵 −ℎ 𝐴) ·ih (𝐷 −ℎ 𝐶)) | ||
Theorem | hi2eq 28810 | Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih (𝐴 −ℎ 𝐵)) = (𝐵 ·ih (𝐴 −ℎ 𝐵)) ↔ 𝐴 = 𝐵)) | ||
Theorem | hial2eq 28811* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝐴 ·ih 𝑥) = (𝐵 ·ih 𝑥) ↔ 𝐴 = 𝐵)) | ||
Theorem | hial2eq2 28812* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝑥 ·ih 𝐴) = (𝑥 ·ih 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | orthcom 28813 | Orthogonality commutes. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 ↔ (𝐵 ·ih 𝐴) = 0)) | ||
Theorem | normlem0 28814 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 7-Oct-1999.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ ⇒ ⊢ ((𝐹 −ℎ (𝑆 ·ℎ 𝐺)) ·ih (𝐹 −ℎ (𝑆 ·ℎ 𝐺))) = (((𝐹 ·ih 𝐹) + (-(∗‘𝑆) · (𝐹 ·ih 𝐺))) + ((-𝑆 · (𝐺 ·ih 𝐹)) + ((𝑆 · (∗‘𝑆)) · (𝐺 ·ih 𝐺)))) | ||
Theorem | normlem1 28815 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 22-Aug-1999.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ & ⊢ 𝑅 ∈ ℝ & ⊢ (abs‘𝑆) = 1 ⇒ ⊢ ((𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺)) ·ih (𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺))) = (((𝐹 ·ih 𝐹) + (((∗‘𝑆) · -𝑅) · (𝐹 ·ih 𝐺))) + (((𝑆 · -𝑅) · (𝐺 ·ih 𝐹)) + ((𝑅↑2) · (𝐺 ·ih 𝐺)))) | ||
Theorem | normlem2 28816 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ & ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) ⇒ ⊢ 𝐵 ∈ ℝ | ||
Theorem | normlem3 28817 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ & ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) & ⊢ 𝐴 = (𝐺 ·ih 𝐺) & ⊢ 𝐶 = (𝐹 ·ih 𝐹) & ⊢ 𝑅 ∈ ℝ ⇒ ⊢ (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶) = (((𝐹 ·ih 𝐹) + (((∗‘𝑆) · -𝑅) · (𝐹 ·ih 𝐺))) + (((𝑆 · -𝑅) · (𝐺 ·ih 𝐹)) + ((𝑅↑2) · (𝐺 ·ih 𝐺)))) | ||
Theorem | normlem4 28818 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ & ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) & ⊢ 𝐴 = (𝐺 ·ih 𝐺) & ⊢ 𝐶 = (𝐹 ·ih 𝐹) & ⊢ 𝑅 ∈ ℝ & ⊢ (abs‘𝑆) = 1 ⇒ ⊢ ((𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺)) ·ih (𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺))) = (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶) | ||
Theorem | normlem5 28819 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Aug-1999.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ & ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) & ⊢ 𝐴 = (𝐺 ·ih 𝐺) & ⊢ 𝐶 = (𝐹 ·ih 𝐹) & ⊢ 𝑅 ∈ ℝ & ⊢ (abs‘𝑆) = 1 ⇒ ⊢ 0 ≤ (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶) | ||
Theorem | normlem6 28820 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ & ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) & ⊢ 𝐴 = (𝐺 ·ih 𝐺) & ⊢ 𝐶 = (𝐹 ·ih 𝐹) & ⊢ (abs‘𝑆) = 1 ⇒ ⊢ (abs‘𝐵) ≤ (2 · ((√‘𝐴) · (√‘𝐶))) | ||
Theorem | normlem7 28821 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.) |
⊢ 𝑆 ∈ ℂ & ⊢ 𝐹 ∈ ℋ & ⊢ 𝐺 ∈ ℋ & ⊢ (abs‘𝑆) = 1 ⇒ ⊢ (((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) ≤ (2 · ((√‘(𝐺 ·ih 𝐺)) · (√‘(𝐹 ·ih 𝐹)))) | ||
Theorem | normlem8 28822 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) ·ih (𝐶 +ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) + ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶))) | ||
Theorem | normlem9 28823 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶))) | ||
Theorem | normlem7tALT 28824 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝑆 ∈ ℂ ∧ (abs‘𝑆) = 1) → (((∗‘𝑆) · (𝐴 ·ih 𝐵)) + (𝑆 · (𝐵 ·ih 𝐴))) ≤ (2 · ((√‘(𝐵 ·ih 𝐵)) · (√‘(𝐴 ·ih 𝐴))))) | ||
Theorem | bcseqi 28825 | Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 28885. (Contributed by NM, 16-Jul-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (((𝐴 ·ih 𝐵) · (𝐵 ·ih 𝐴)) = ((𝐴 ·ih 𝐴) · (𝐵 ·ih 𝐵)) ↔ ((𝐵 ·ih 𝐵) ·ℎ 𝐴) = ((𝐴 ·ih 𝐵) ·ℎ 𝐵)) | ||
Theorem | normlem9at 28826 | 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 28827 | 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 28828 | 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 28829 | 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 28830 | Real closure of the norm of a vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (normℎ‘𝐴) ∈ ℝ) | ||
Theorem | normge0 28831 | The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → 0 ≤ (normℎ‘𝐴)) | ||
Theorem | normgt0 28832 | The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 ≠ 0ℎ ↔ 0 < (normℎ‘𝐴))) | ||
Theorem | norm0 28833 | The norm of a zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (normℎ‘0ℎ) = 0 | ||
Theorem | norm-i 28834 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ)) | ||
Theorem | normne0 28835 | 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 28836 | Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (normℎ‘𝐴) ∈ ℝ | ||
Theorem | normsqi 28837 | The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴) | ||
Theorem | norm-i-i 28838 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 5-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ) | ||
Theorem | normsq 28839 | The square of a norm. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴)) | ||
Theorem | normsub0i 28840 | 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 28841 | 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 28842 | 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 28843 | 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 28844 | Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵)) | ||
Theorem | norm-iii 28845 | Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵))) | ||
Theorem | normsubi 28846 | 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 28847 | 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 28848 | 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 28849 | 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 28850 | 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 28851 | 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 28852 | 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 28853 | 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 28854 | 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 28855 | 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 28856 | Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐶 −ℎ 𝐴)) + (normℎ‘(𝐶 −ℎ 𝐵)))) | ||
Theorem | norm3lemt 28857 | 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 28858 | 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 28859 | 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 28860 | 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 28861 | 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 28862 | 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 28863 | 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 28789. (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 28864 | 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 28789. (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 28865 | Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
⊢ +ℎ ∈ AbelOp | ||
Theorem | hilid 28866 | 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 28867 | 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 28868 | 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 28869 | 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 28870 | Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
Theorem | hhva 28871 | The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
Theorem | hhba 28872 | The base set of Hilbert space. This theorem provides an independent proof of df-hba 28674 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ ℋ = (BaseSet‘𝑈) | ||
Theorem | hh0v 28873 | 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 28874 | The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
Theorem | hhvs 28875 | The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ −ℎ = ( −𝑣 ‘𝑈) | ||
Theorem | hhnm 28876 | The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
Theorem | hhims 28877 | The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 = (IndMet‘𝑈) | ||
Theorem | hhims2 28878 | Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 = (normℎ ∘ −ℎ ) | ||
Theorem | hhmet 28879 | The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (Met‘ ℋ) | ||
Theorem | hhxmet 28880 | The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ 𝐷 ∈ (∞Met‘ ℋ) | ||
Theorem | hhmetdval 28881 | 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 28882 | 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 28883 | 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 28884 | 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 28885 | 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 28886 | 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 28887 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 28885. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐵)) | ||
Theorem | bcs3 28888 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 28885. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐵) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐴)) | ||
Theorem | hcau 28889* | 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 28890 | 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 28891* | 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 28892* | 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 28893* | 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 28894 | 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 28895 | Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹 ⇝𝑣 𝐴 → 𝐴 ∈ ℋ) | ||
Theorem | hlimconvi 28896* | 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 28897* | 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 28898* | 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 28899 | The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (Met‘ ℋ) | ||
Theorem | hilxmet 28900 | The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
⊢ 𝐷 = (normℎ ∘ −ℎ ) ⇒ ⊢ 𝐷 ∈ (∞Met‘ ℋ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |