Home | Metamath
Proof Explorer Theorem List (p. 228 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 | clmvs1 22701 | Scalar product with ring unit. (lmodvs1 18714 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (1 · 𝑋) = 𝑋) | ||
Theorem | clmvs2 22702 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (𝐴 + 𝐴) = (2 · 𝐴)) | ||
Theorem | clm0vs 22703 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 18719 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (0 · 𝑋) = 0 ) | ||
Theorem | clmopfne 22704 | The (functionalized) operations of a complex left module cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 3-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + ≠ · ) | ||
Theorem | isclmp 22705* | The predicate "is a complex left module space." (Contributed by NM, 31-May-2008.) (Revised by AV, 4-Oct-2021.) |
⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑊 ∈ ℂMod ↔ ((𝑊 ∈ Grp ∧ 𝑆 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) ∧ ∀𝑥 ∈ 𝑉 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) | ||
Theorem | isclmi0 22706* | Properties that determine a complex left module. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 4-Oct-2021.) |
⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (ℂfld ↾s 𝐾) & ⊢ 𝑊 ∈ Grp & ⊢ 𝐾 ∈ (SubRing‘ℂfld) & ⊢ (𝑥 ∈ 𝑉 → (1 · 𝑥) = 𝑥) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → (𝑦 · 𝑥) ∈ 𝑉) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → ((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥))) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))) ⇒ ⊢ 𝑊 ∈ ℂMod | ||
Theorem | clmvneg1 22707 | Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 18729 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (-1 · 𝑋) = (𝑁‘𝑋)) | ||
Theorem | clmvsneg 22708 | Multiplication of a vector by a negated scalar. (lmodvsneg 18730 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = (-𝑅 · 𝑋)) | ||
Theorem | clmmulg 22709 | The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ∙ = (.g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵)) | ||
Theorem | clmsubdir 22710 | Scalar multiplication distributive law for subtraction. (lmodsubdir 18744 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋))) | ||
Theorem | clmpm1dir 22711 | Subtractive distributive law for the scalar product of a complex left module. (Contributed by NM, 31-Jul-2007.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐾 = (Base‘(Scalar‘𝑊)) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (-1 · (𝐵 · 𝐶)))) | ||
Theorem | clmnegneg 22712 | Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (-1 · (-1 · 𝐴)) = 𝐴) | ||
Theorem | clmnegsubdi2 22713 | Distribution of negative over vector subtraction. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 29-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (-1 · (𝐴 + (-1 · 𝐵))) = (𝐵 + (-1 · 𝐴))) | ||
Theorem | clmsub4 22714 | Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 5-Aug-2007.) (Revised by AV, 29-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 + 𝐵) + (-1 · (𝐶 + 𝐷))) = ((𝐴 + (-1 · 𝐶)) + (𝐵 + (-1 · 𝐷)))) | ||
Theorem | clmvsrinv 22715 | A vector minus itself. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 28-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (𝐴 + (-1 · 𝐴)) = 0 ) | ||
Theorem | clmvslinv 22716 | Minus a vector plus itself. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 28-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → ((-1 · 𝐴) + 𝐴) = 0 ) | ||
Theorem | clmvsubval 22717 | Value of vector subtraction in terms of addition in a complex module. (lmodvsubval2 18741 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵))) | ||
Theorem | clmvsubval2 22718 | Value of vector subtraction on a complex module. (Contributed by Mario Carneiro, 19-Nov-2013.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = ((-1 · 𝐵) + 𝐴)) | ||
Theorem | clmvz 22719 | Two ways to express the negative of a vector. (Contributed by NM, 29-Feb-2008.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → ( 0 − 𝐴) = (-1 · 𝐴)) | ||
Theorem | zlmclm 22720 | The ℤ-module operation turns an arbitrary abelian group into a complex module. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod) | ||
Theorem | clmzlmvsca 22721 | The scalar product of a complex module matches the scalar product of the derived ℤ-module, which implies, together with zlmbas 19685 and zlmplusg 19686, that any module over ℤ is structure-equivalent to the canonical ℤ-module ℤMod‘𝐺. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ ℂMod ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑋)) → (𝐴( ·𝑠 ‘𝐺)𝐵) = (𝐴( ·𝑠 ‘𝑊)𝐵)) | ||
Theorem | nmoleub2lem 22722* | Lemma for nmoleub2a 22725 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → 0 ≤ 𝐴) & ⊢ ((((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) ∧ (𝑦 ∈ 𝑉 ∧ 𝑦 ≠ (0g‘𝑆))) → (𝑀‘(𝐹‘𝑦)) ≤ (𝐴 · (𝐿‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝜓 → (𝐿‘𝑥) ≤ 𝑅)) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) | ||
Theorem | nmoleub2lem3 22723* | Lemma for nmoleub2a 22725 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ℚ ⊆ 𝐾) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ (0g‘𝑆)) & ⊢ (𝜑 → ((𝑟 · 𝐵) ∈ 𝑉 → ((𝐿‘(𝑟 · 𝐵)) < 𝑅 → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴))) & ⊢ (𝜑 → ¬ (𝑀‘(𝐹‘𝐵)) ≤ (𝐴 · (𝐿‘𝐵))) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | nmoleub2lem2 22724* | Lemma for nmoleub2a 22725 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ℚ ⊆ 𝐾) & ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥)𝑂𝑅 → (𝐿‘𝑥) ≤ 𝑅)) & ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥) < 𝑅 → (𝐿‘𝑥)𝑂𝑅)) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥)𝑂𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) | ||
Theorem | nmoleub2a 22725* | The operator norm is the supremum of the value of a linear operator in the closed unit ball. (Contributed by Mario Carneiro, 19-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ℚ ⊆ 𝐾) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥) ≤ 𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) | ||
Theorem | nmoleub2b 22726* | The operator norm is the supremum of the value of a linear operator in the open unit ball. (Contributed by Mario Carneiro, 19-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ℚ ⊆ 𝐾) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥) < 𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) | ||
Theorem | nmoleub3 22727* | The operator norm is the supremum of the value of a linear operator on the closed unit sphere. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → ℝ ⊆ 𝐾) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥) = 𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) | ||
Theorem | nmhmcn 22728 | A linear operator over a normed complex module is bounded iff it is continuous. (Contributed by Mario Carneiro, 22-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐾 = (TopOpen‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝑆 ∈ (NrmMod ∩ ℂMod) ∧ 𝑇 ∈ (NrmMod ∩ ℂMod) ∧ ℚ ⊆ 𝐵) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)))) | ||
Theorem | cmodscexp 22729 | The powers of i belong to the scalar subring of a complex module if i belongs to the scalar subring . (Contributed by AV, 18-Oct-2021.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂMod ∧ i ∈ 𝐾) ∧ 𝑁 ∈ ℕ) → (i↑𝑁) ∈ 𝐾) | ||
Theorem | cmodscmulexp 22730 | The scalar product of a vector with powers of i belongs to the base set of a complex module if the scalar subring of th complex module contains i. (Contributed by AV, 18-Oct-2021.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ)) → ((i↑𝑁) · 𝐵) ∈ 𝑋) | ||
Usually, "complex vector spaces" are vector spaces over the field of the complex numbers, see for example the definition in [Roman] p. 36. In the following, however, the class ℂVec of "complex vector spaces" is generalized to include all vector spaces over subrings of the field of the complex numbers which are division rings (see iscvs 22735). This is analogous to the definition ℂMod of "complex left modules", which are left modules over arbitrary subrings of the field of the complex numbers. Therefore, the real vector spaces (see recvs 22754) and even the rational vector spaces (see qcvs 22755) also belong to ℂVec. So that ZZ-modules (that are the same as Abelian groups, see zlmclm 22720) are complex left modules, but are not complex vector spaces with our definitions (see zclmncvs 22756), because the ring ZZ is not a division subring of CC, see zringndrg 19657. | ||
Syntax | ccvs 22731 | Complex vector space. |
class ℂVec | ||
Definition | df-cvs 22732 | Define a complex vector space, which is just a complex left module and a vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ ℂVec = (ℂMod ∩ LVec) | ||
Theorem | cvslvec 22733 | A complex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ (𝜑 → 𝑊 ∈ ℂVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ LVec) | ||
Theorem | cvsclm 22734 | A complex vector space is a complex left module. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ (𝜑 → 𝑊 ∈ ℂVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ ℂMod) | ||
Theorem | iscvs 22735 | A complex vector space is a complex left module over a division ring. For example, the (complex) left modules over the rational or real or complex numbers are complex vector spaces. (Contributed by AV, 4-Oct-2021.) |
⊢ (𝑊 ∈ ℂVec ↔ (𝑊 ∈ ℂMod ∧ (Scalar‘𝑊) ∈ DivRing)) | ||
Theorem | iscvsp 22736* | The predicate "is a complex vector space." (Contributed by NM, 31-May-2008.) (Revised by AV, 4-Oct-2021.) |
⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑊 ∈ ℂVec ↔ ((𝑊 ∈ Grp ∧ (𝑆 ∈ DivRing ∧ 𝑆 = (ℂfld ↾s 𝐾)) ∧ 𝐾 ∈ (SubRing‘ℂfld)) ∧ ∀𝑥 ∈ 𝑉 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝐾 ((𝑦 · 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑉 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝐾 (((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥)) ∧ ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))))))) | ||
Theorem | iscvsi 22737* | Properties that determine a complex vector space. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 4-Oct-2021.) |
⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 ∈ Grp & ⊢ 𝑆 = (ℂfld ↾s 𝐾) & ⊢ 𝑆 ∈ DivRing & ⊢ 𝐾 ∈ (SubRing‘ℂfld) & ⊢ (𝑥 ∈ 𝑉 → (1 · 𝑥) = 𝑥) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → (𝑦 · 𝑥) ∈ 𝑉) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → ((𝑧 + 𝑦) · 𝑥) = ((𝑧 · 𝑥) + (𝑦 · 𝑥))) & ⊢ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → ((𝑧 · 𝑦) · 𝑥) = (𝑧 · (𝑦 · 𝑥))) ⇒ ⊢ 𝑊 ∈ ℂVec | ||
Theorem | cvsi 22738* | The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑆 = (Base‘(Scalar‘𝑊)) & ⊢ ∙ = ( ·sf ‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂVec → (𝑊 ∈ Abel ∧ (𝑆 ⊆ ℂ ∧ ∙ :(𝑆 × 𝑋)⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))))) | ||
Theorem | cvsunit 22739 | Unit group of the scalar ring of a complex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂVec → (𝐾 ∖ {0}) = (Unit‘𝐹)) | ||
Theorem | cvsdiv 22740 | Division of the scalar ring of a complex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) = (𝐴(/r‘𝐹)𝐵)) | ||
Theorem | cvsdivcl 22741 | The scalar field of a complex vector space is closed under division. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ∈ 𝐾) | ||
Theorem | cvsmuleqdivd 22742 | An equality involving ratios in a complex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → (𝐴 · 𝑋) = (𝐵 · 𝑌)) ⇒ ⊢ (𝜑 → 𝑋 = ((𝐵 / 𝐴) · 𝑌)) | ||
Theorem | cvsdiveqd 22743 | An equality involving ratios in a complex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑋 = ((𝐴 / 𝐵) · 𝑌)) ⇒ ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = 𝑌) | ||
Theorem | cnlmodlem1 22744 | Lemma 1 for cnlmod 22748. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (Base‘𝑊) = ℂ | ||
Theorem | cnlmodlem2 22745 | Lemma 2 for cnlmod 22748. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (+g‘𝑊) = + | ||
Theorem | cnlmodlem3 22746 | Lemma 3 for cnlmod 22748. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (Scalar‘𝑊) = ℂfld | ||
Theorem | cnlmod4 22747 | Lemma 4 for cnlmod 22748. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( ·𝑠 ‘𝑊) = · | ||
Theorem | cnlmod 22748 | The set of complex numbers is a left module over itself. The vector operation is +, and the scalar product is ·. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ 𝑊 ∈ LMod | ||
Theorem | cnstrcvs 22749 | The set of complex numbers is a complex vector space. The vector operation is +, and the scalar product is ·. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ 𝑊 ∈ ℂVec | ||
Theorem | cnrbas 22750 | The set of complex numbers is the base set of the complex numbers as left module induced by the complex numbers as subring of itself. (Contributed by AV, 21-Sep-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ (Base‘𝐶) = ℂ | ||
Theorem | cnrlmod 22751 | The set of complex numbers (as a subring of itself) is a left module over itself. The vector operation is +, and the scalar product is ·. (Contributed by AV, 21-Sep-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ LMod | ||
Theorem | cnrlvec 22752 | The set of complex numbers (as a subring of itself) is a (left) vector space over itself. The vector operation is +, and the scalar product is ·. (Contributed by AV, 21-Sep-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ LVec | ||
Theorem | cncvs 22753 | The set of complex numbers (as a subring of itself) is a complex vector space. The vector operation is +, and the scalar product is ·. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ ℂVec | ||
Theorem | recvs 22754 | The set of real numbers (as a subring of itself) is a complex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) |
⊢ 𝑅 = (ringLMod‘ℝfld) ⇒ ⊢ 𝑅 ∈ ℂVec | ||
Theorem | qcvs 22755 | The set of rational numbers (as a subring of itself) is a complex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) |
⊢ 𝑄 = (ringLMod‘(ℂfld ↾s ℚ)) ⇒ ⊢ 𝑄 ∈ ℂVec | ||
Theorem | zclmncvs 22756 | The set of integers (as a subring of itself) is a complex module, but not a complex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) |
⊢ 𝑍 = (ringLMod‘ℤring) ⇒ ⊢ (𝑍 ∈ ℂMod ∧ 𝑍 ∉ ℂVec) | ||
Until now, there is no need for a definition of normed complex vector spaces. The idiom 𝑊 ∈ (NrmVec ∩ ℂVec) is used in the following to say that 𝑊 is a normed complex vector space, i.e. a complex vector space which is also a normed vector space. The label of the theorems for normed complex vector spaces contain the fragment ncvs. | ||
Theorem | isncvsngp 22757* | The predicate "is a normed complex vector space." if the underlying group is a normed group. (Contributed by NM, 5-Jun-2008.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ (NrmVec ∩ ℂVec) ↔ (𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))) | ||
Theorem | isncvsngpd 22758* | Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂVec) & ⊢ (𝜑 → 𝑊 ∈ NrmGrp) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) → (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) ⇒ ⊢ (𝜑 → 𝑊 ∈ (NrmVec ∩ ℂVec)) | ||
Theorem | ncvsi 22759* | The properties of a normed complex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ (NrmVec ∩ ℂVec) → (𝑊 ∈ ℂVec ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) | ||
Theorem | ncvsprp 22760 | Proportionality property of the norm of a scalar product in a normed complex vector space. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → (𝑁‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (𝑁‘𝐵))) | ||
Theorem | ncvsge0 22761 | The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴 ∈ (𝐾 ∩ ℝ) ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ 𝑉) → (𝑁‘(𝐴 · 𝐵)) = (𝐴 · (𝑁‘𝐵))) | ||
Theorem | ncvsm1 22762 | The norm of the negative of a vector. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ 𝐴 ∈ 𝑉) → (𝑁‘(-1 · 𝐴)) = (𝑁‘𝐴)) | ||
Theorem | ncvsdif 22763 | The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑁‘(𝐴 + (-1 · 𝐵))) = (𝑁‘(𝐵 + (-1 · 𝐴)))) | ||
Theorem | ncvspi 22764 | The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝑁‘(𝐴 + (i · 𝐵))) = (𝑁‘(𝐵 + (-i · 𝐴)))) | ||
Theorem | ncvs1 22765 | From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = ( ·𝑠 ‘𝐺) & ⊢ 𝐹 = (Scalar‘𝐺) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝐺 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝑁‘((1 / (𝑁‘𝐴)) · 𝐴)) = 1) | ||
Theorem | cnrnvc 22766 | The set of complex numbers (as a subring of itself) is a normed vector space over itself. The vector operation is +, and the scalar product is ·, and the norm function is abs. (Contributed by AV, 9-Oct-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ NrmVec | ||
Theorem | cnncvs 22767 | The set of complex numbers (as a subring of itself) is a normed complex vector space. The vector operation is +, and the scalar product is ·, and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ (NrmVec ∩ ℂVec) | ||
Theorem | cnnm 22768 | The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ (norm‘𝐶) = abs | ||
Theorem | ncvspds 22769 | Value of the distance function in terms of the norm of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 13-Oct-2021.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ (NrmVec ∩ ℂVec) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴 + (-1 · 𝐵)))) | ||
Theorem | cnindmet 22770 | The metric induced on the complex numbers. cnmet 22385 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 19577 and also cnmet 22385. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.) |
⊢ 𝑇 = (ℂfld toNrmGrp abs) ⇒ ⊢ (dist‘𝑇) = (abs ∘ − ) | ||
Theorem | cnncvsaddassdemo 22771 | Derive the associative law for complex number addition addass 9902 to demonstrate the use of the properties of a (normed complex) vector space for the complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | cnncvsmulassdemo 22772 | Derive the associative law for complex number multiplication mulass 9903 interpreted as scalar multiplication to demonstrate the use of the properties of a (normed) complex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | cnncvsabsnegdemo 22773 | Derive the absolute value of a negative complex number absneg 13865 to demonstrate the use of the properties of a normed complex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴)) | ||
Syntax | ccph 22774 | Extend class notation with a complex pre-Hilbert space. |
class ℂPreHil | ||
Syntax | ctch 22775 | Function to put a norm on a Hilbert space. |
class toℂHil | ||
Definition | df-cph 22776* | Define a complex pre-Hilbert space. By restricting the scalar field to a quadratically closed subfield of ℂ, we have enough structure to define a norm, with the associated connection to a metric and topology. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))} | ||
Definition | df-tch 22777* | Define a function to augment a (pre-)Hilbert space with a norm. No extra parameters are needed, but some conditions must be satisfied to ensure that this in fact creates a normed pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ toℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))) | ||
Theorem | iscph 22778* | A complex pre-Hilbert space is a pre-Hilbert space over a quadratically closed subfield of the complex numbers, with a norm defined. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld ↾s 𝐾)) ∧ (√ “ (𝐾 ∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))) | ||
Theorem | cphphl 22779 | A complex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil) | ||
Theorem | cphnlm 22780 | A complex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod) | ||
Theorem | cphngp 22781 | A complex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp) | ||
Theorem | cphlmod 22782 | A complex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod) | ||
Theorem | cphlvec 22783 | A complex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LVec) | ||
Theorem | cphnvc 22784 | A complex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmVec) | ||
Theorem | cphsubrglem 22785 | Lemma for cphsubrg 22788. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴)) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → (𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 = (𝐴 ∩ ℂ) ∧ 𝐾 ∈ (SubRing‘ℂfld))) | ||
Theorem | cphreccllem 22786 | Lemma for cphreccl 22789. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴)) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0) → (1 / 𝑋) ∈ 𝐾) | ||
Theorem | cphsca 22787 | A complex pre-Hilbert space is a vector space over a subfield of ℂ. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝐹 = (ℂfld ↾s 𝐾)) | ||
Theorem | cphsubrg 22788 | The scalar field of a complex pre-Hilbert space is a subring of ℂ. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝐾 ∈ (SubRing‘ℂfld)) | ||
Theorem | cphreccl 22789 | The scalar field of a complex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ 𝐾) | ||
Theorem | cphdivcl 22790 | The scalar field of a complex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ∈ 𝐾) | ||
Theorem | cphcjcl 22791 | The scalar field of a complex pre-Hilbert space is closed under conjugation. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾) → (∗‘𝐴) ∈ 𝐾) | ||
Theorem | cphsqrtcl 22792 | The scalar field of a complex pre-Hilbert space is closed under square roots of positive reals (i.e. it is quadratically closed relative to ℝ). (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (√‘𝐴) ∈ 𝐾) | ||
Theorem | cphabscl 22793 | The scalar field of a complex pre-Hilbert space is closed under the absolute value operation. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾) → (abs‘𝐴) ∈ 𝐾) | ||
Theorem | cphsqrtcl2 22794 | The scalar field of a complex pre-Hilbert space is closed under square roots of all numbers except possibly the negative reals. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) → (√‘𝐴) ∈ 𝐾) | ||
Theorem | cphsqrtcl3 22795 | If the scalar field contains i, it is completely closed under square roots (i.e. it is quadratically closed). (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾) → (√‘𝐴) ∈ 𝐾) | ||
Theorem | cphqss 22796 | The scalar field of a complex pre-Hilbert space contains all rational numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → ℚ ⊆ 𝐾) | ||
Theorem | cphclm 22797 | A complex pre-Hilbert space is a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod) | ||
Theorem | cphnmvs 22798 | Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((abs‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | cphipcl 22799 | An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ ℂ) | ||
Theorem | cphnmfval 22800* | The value of the norm in a complex pre-Hilbert space is the square root of the inner product of a vector with itself. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |