![]() |
Metamath
Proof Explorer Theorem List (p. 238 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clmopfne 23701 | The (functionalized) operations of addition and multiplication by a scalar of a subcomplex module cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 3-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + ≠ · ) | ||
Theorem | isclmp 23702* | The predicate "is a subcomplex module". (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 23703* | Properties that determine a subcomplex 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 23704 | Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 19670 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (-1 · 𝑋) = (𝑁‘𝑋)) | ||
Theorem | clmvsneg 23705 | Multiplication of a vector by a negated scalar. (lmodvsneg 19671 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = (-𝑅 · 𝑋)) | ||
Theorem | clmmulg 23706 | The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ∙ = (.g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵)) | ||
Theorem | clmsubdir 23707 | Scalar multiplication distributive law for subtraction. (lmodsubdir 19685 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋))) | ||
Theorem | clmpm1dir 23708 | Subtractive distributive law for the scalar product of a subcomplex module. (Contributed by NM, 31-Jul-2007.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐾 = (Base‘(Scalar‘𝑊)) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (-1 · (𝐵 · 𝐶)))) | ||
Theorem | clmnegneg 23709 | Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (-1 · (-1 · 𝐴)) = 𝐴) | ||
Theorem | clmnegsubdi2 23710 | 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 23711 | 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 23712 | 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 23713 | 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 23714 | Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 19682. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵))) | ||
Theorem | clmvsubval2 23715 | Value of vector subtraction on a subcomplex module. (Contributed by Mario Carneiro, 19-Nov-2013.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = ((-1 · 𝐵) + 𝐴)) | ||
Theorem | clmvz 23716 | 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 23717 | The ℤ-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod) | ||
Theorem | clmzlmvsca 23718 | The scalar product of a subcomplex module matches the scalar product of the derived ℤ-module, which implies, together with zlmbas 20211 and zlmplusg 20212, that any module over ℤ is structure-equivalent to the canonical ℤ-module ℤMod‘𝐺. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ ℂMod ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑋)) → (𝐴( ·𝑠 ‘𝐺)𝐵) = (𝐴( ·𝑠 ‘𝑊)𝐵)) | ||
Theorem | nmoleub2lem 23719* | Lemma for nmoleub2a 23722 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 23720* | Lemma for nmoleub2a 23722 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 23721* | Lemma for nmoleub2a 23722 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ℚ ⊆ 𝐾) & ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥)𝑂𝑅 → (𝐿‘𝑥) ≤ 𝑅)) & ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥) < 𝑅 → (𝐿‘𝑥)𝑂𝑅)) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥)𝑂𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) | ||
Theorem | nmoleub2a 23722* | 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 23723* | 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 23724* | The operator norm is the supremum of the value of a linear operator on the 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 23725 | A linear operator over a normed subcomplex 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 23726 | The powers of i belong to the scalar subring of a subcomplex module if i belongs to the scalar subring . (Contributed by AV, 18-Oct-2021.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂMod ∧ i ∈ 𝐾) ∧ 𝑁 ∈ ℕ) → (i↑𝑁) ∈ 𝐾) | ||
Theorem | cmodscmulexp 23727 | The scalar product of a vector with powers of i belongs to the base set of a subcomplex module if the scalar subring of th subcomplex 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 setting of set.mm, it is convenient to consider collectively vector spaces on subfields of the field of complex numbers. We call these, "subcomplex vector spaces" and collect them in the class ℂVec defined in df-cvs 23729 and characterized in iscvs 23732. These include rational vector spaces (qcvs 23752), real vector spaces (recvs 23751) and complex vector spaces (cncvs 23750). This definition is analogous to the definition of subcomplex modules (and their class ℂMod), which are modules over subrings of the field of complex numbers. Note that ZZ-modules (that are roughly the same thing as Abelian groups, see zlmclm 23717) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 23753), because the ring ZZ is not a division ring (see zringndrg 20183). Since the field of complex numbers is commutative, so are its subrings, so there is no need to explicitly state "left module" or "left vector space" for subcomplex modules or vector spaces. | ||
Syntax | ccvs 23728 | Syntax for the class of subcomplex vector spaces. |
class ℂVec | ||
Definition | df-cvs 23729 | Define the class of subcomplex vector spaces, which are the subcomplex modules which are also vector spaces. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ ℂVec = (ℂMod ∩ LVec) | ||
Theorem | cvslvec 23730 | A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ (𝜑 → 𝑊 ∈ ℂVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ LVec) | ||
Theorem | cvsclm 23731 | A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ (𝜑 → 𝑊 ∈ ℂVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ ℂMod) | ||
Theorem | iscvs 23732 | A subcomplex vector space is a subcomplex module over a division ring. For example, the subcomplex modules over the rational or real or complex numbers are subcomplex vector spaces. (Contributed by AV, 4-Oct-2021.) |
⊢ (𝑊 ∈ ℂVec ↔ (𝑊 ∈ ℂMod ∧ (Scalar‘𝑊) ∈ DivRing)) | ||
Theorem | iscvsp 23733* | The predicate "is a subcomplex 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 23734* | Properties that determine a subcomplex 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 23735* | The properties of a subcomplex 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 23736 | Unit group of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂVec → (𝐾 ∖ {0}) = (Unit‘𝐹)) | ||
Theorem | cvsdiv 23737 | Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) = (𝐴(/r‘𝐹)𝐵)) | ||
Theorem | cvsdivcl 23738 | The scalar field of a subcomplex vector space is closed under division. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ∈ 𝐾) | ||
Theorem | cvsmuleqdivd 23739 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → (𝐴 · 𝑋) = (𝐵 · 𝑌)) ⇒ ⊢ (𝜑 → 𝑋 = ((𝐵 / 𝐴) · 𝑌)) | ||
Theorem | cvsdiveqd 23740 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑋 = ((𝐴 / 𝐵) · 𝑌)) ⇒ ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = 𝑌) | ||
Theorem | cnlmodlem1 23741 | Lemma 1 for cnlmod 23745. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (Base‘𝑊) = ℂ | ||
Theorem | cnlmodlem2 23742 | Lemma 2 for cnlmod 23745. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (+g‘𝑊) = + | ||
Theorem | cnlmodlem3 23743 | Lemma 3 for cnlmod 23745. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (Scalar‘𝑊) = ℂfld | ||
Theorem | cnlmod4 23744 | Lemma 4 for cnlmod 23745. (Contributed by AV, 20-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( ·𝑠 ‘𝑊) = · | ||
Theorem | cnlmod 23745 | 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 23746 | The set of complex numbers is a subcomplex 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 23747 | The set of complex numbers is the base set of the complex left module of complex numbers. (Contributed by AV, 21-Sep-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ (Base‘𝐶) = ℂ | ||
Theorem | cnrlmod 23748 | The complex left module of complex numbers is a left module. The vector operation is +, and the scalar product is ·. (Contributed by AV, 21-Sep-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ LMod | ||
Theorem | cnrlvec 23749 | The complex left module of complex numbers is a left vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 21-Sep-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ LVec | ||
Theorem | cncvs 23750 | The complex left module of complex numbers is a subcomplex 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 23751 | The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) |
⊢ 𝑅 = (ringLMod‘ℝfld) ⇒ ⊢ 𝑅 ∈ ℂVec | ||
Theorem | qcvs 23752 | The field of rational numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) |
⊢ 𝑄 = (ringLMod‘(ℂfld ↾s ℚ)) ⇒ ⊢ 𝑄 ∈ ℂVec | ||
Theorem | zclmncvs 23753 | The ring of integers as left module over itself is a subcomplex module, but not a subcomplex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) |
⊢ 𝑍 = (ringLMod‘ℤring) ⇒ ⊢ (𝑍 ∈ ℂMod ∧ 𝑍 ∉ ℂVec) | ||
This section characterizes normed subcomplex vector spaces as subcomplex vector spaces which are also normed vector spaces (that is, normed groups with a positively homogeneous norm). For the moment, there is no need of a special token to represent their class, so we only use the characterization isncvsngp 23754. Most theorems for normed subcomplex vector spaces have a label containing "ncvs". The idiom 𝑊 ∈ (NrmVec ∩ ℂVec) is used in the following to say that 𝑊 is a normed subcomplex vector space, i.e., a subcomplex vector space which is also a normed vector space. | ||
Theorem | isncvsngp 23754* | A normed subcomplex vector space is a subcomplex vector space which is a normed group with a positively homogeneous norm. (Contributed by NM, 5-Jun-2008.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ (NrmVec ∩ ℂVec) ↔ (𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))) | ||
Theorem | isncvsngpd 23755* | Properties that determine a normed subcomplex 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 23756* | The properties of a normed subcomplex 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 23757 | Proportionality property of the norm of a scalar product in a normed subcomplex vector space. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → (𝑁‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (𝑁‘𝐵))) | ||
Theorem | ncvsge0 23758 | 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 23759 | The norm of the opposite of a vector. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 8-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ 𝐴 ∈ 𝑉) → (𝑁‘(-1 · 𝐴)) = (𝑁‘𝐴)) | ||
Theorem | ncvsdif 23760 | 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 23761 | 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 23762 | From any nonzero vector of a normed subcomplex vector space, construct a collinear 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 23763 | The module of complex numbers (as a module over 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 23764 | The module of complex numbers (as a module over itself) is a normed subcomplex vector space. The vector operation is +, the scalar product is ·, and the norm is abs (see cnnm 23765) . (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ (NrmVec ∩ ℂVec) | ||
Theorem | cnnm 23765 | The norm of the normed subcomplex vector space of complex numbers is the absolute value. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) |
⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ (norm‘𝐶) = abs | ||
Theorem | ncvspds 23766 | Value of the distance function in terms of the norm of a normed subcomplex 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 23767 | The metric induced on the complex numbers. cnmet 23377 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 20101 and also cnmet 23377. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.) |
⊢ 𝑇 = (ℂfld toNrmGrp abs) ⇒ ⊢ (dist‘𝑇) = (abs ∘ − ) | ||
Theorem | cnncvsaddassdemo 23768 | Derive the associative law for complex number addition addass 10613 to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | cnncvsmulassdemo 23769 | Derive the associative law for complex number multiplication mulass 10614 interpreted as scalar multiplication to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | cnncvsabsnegdemo 23770 | Derive the absolute value of a negative complex number absneg 14629 to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴)) | ||
Syntax | ccph 23771 | Extend class notation with the class of subcomplex pre-Hilbert spaces. |
class ℂPreHil | ||
Syntax | ctcph 23772 | Function to put a norm on a pre-Hilbert space. |
class toℂPreHil | ||
Definition | df-cph 23773* | Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a subfield of ℂfld closed under square roots of nonnegative reals, 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-tcph 23774* | 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 subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))) | ||
Theorem | iscph 23775* | A subcomplex pre-Hilbert space is exactly a pre-Hilbert space over a subfield of the field of complex numbers closed under square roots of nonnegative reals equipped with a norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld ↾s 𝐾)) ∧ (√ “ (𝐾 ∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))) | ||
Theorem | cphphl 23776 | A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil) | ||
Theorem | cphnlm 23777 | A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod) | ||
Theorem | cphngp 23778 | A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp) | ||
Theorem | cphlmod 23779 | A subcomplex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod) | ||
Theorem | cphlvec 23780 | A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LVec) | ||
Theorem | cphnvc 23781 | A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmVec) | ||
Theorem | cphsubrglem 23782 | Lemma for cphsubrg 23785. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴)) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → (𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 = (𝐴 ∩ ℂ) ∧ 𝐾 ∈ (SubRing‘ℂfld))) | ||
Theorem | cphreccllem 23783 | Lemma for cphreccl 23786. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴)) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0) → (1 / 𝑋) ∈ 𝐾) | ||
Theorem | cphsca 23784 | A subcomplex pre-Hilbert space is a vector space over a subfield of ℂfld. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝐹 = (ℂfld ↾s 𝐾)) | ||
Theorem | cphsubrg 23785 | The scalar field of a subcomplex pre-Hilbert space is a subring of ℂfld. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝐾 ∈ (SubRing‘ℂfld)) | ||
Theorem | cphreccl 23786 | The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ 𝐾) | ||
Theorem | cphdivcl 23787 | The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ∈ 𝐾) | ||
Theorem | cphcjcl 23788 | The scalar field of a subcomplex pre-Hilbert space is closed under conjugation. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾) → (∗‘𝐴) ∈ 𝐾) | ||
Theorem | cphsqrtcl 23789 | The scalar field of a subcomplex pre-Hilbert space is closed under square roots of nonnegative reals. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (√‘𝐴) ∈ 𝐾) | ||
Theorem | cphabscl 23790 | The scalar field of a subcomplex pre-Hilbert space is closed under the absolute value operation. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾) → (abs‘𝐴) ∈ 𝐾) | ||
Theorem | cphsqrtcl2 23791 | The scalar field of a subcomplex 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 23792 | If the scalar field of a subcomplex pre-Hilbert space contains the imaginary unit i, then it is closed under square roots (i.e., it is quadratically closed). (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾) → (√‘𝐴) ∈ 𝐾) | ||
Theorem | cphqss 23793 | The scalar field of a subcomplex pre-Hilbert space contains the rational numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → ℚ ⊆ 𝐾) | ||
Theorem | cphclm 23794 | A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod) | ||
Theorem | cphnmvs 23795 | Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((abs‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | cphipcl 23796 | An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ ℂ) | ||
Theorem | cphnmfval 23797* | The value of the norm in a subcomplex 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 → 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) | ||
Theorem | cphnm 23798 | The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝑁‘𝐴) = (√‘(𝐴 , 𝐴))) | ||
Theorem | nmsq 23799 | The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. Equation I4 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ((𝑁‘𝐴)↑2) = (𝐴 , 𝐴)) | ||
Theorem | cphnmf 23800 | The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝑁:𝑉⟶𝐾) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |