| Metamath
Proof Explorer Theorem List (p. 252 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | clmgrp 25101 | A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp) | ||
| Theorem | clmabl 25102 | A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel) | ||
| Theorem | clmring 25103 | The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Ring) | ||
| Theorem | clmfgrp 25104 | The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp) | ||
| Theorem | clm0 25105 | The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘𝐹)) | ||
| Theorem | clm1 25106 | The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 1 = (1r‘𝐹)) | ||
| Theorem | clmadd 25107 | The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + = (+g‘𝐹)) | ||
| Theorem | clmmul 25108 | The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → · = (.r‘𝐹)) | ||
| Theorem | clmcj 25109 | The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → ∗ = (*𝑟‘𝐹)) | ||
| Theorem | isclmi 25110 | Reverse direction of isclm 25097. (Contributed by Mario Carneiro, 30-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) → 𝑊 ∈ ℂMod) | ||
| Theorem | clmzss 25111 | The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → ℤ ⊆ 𝐾) | ||
| Theorem | clmsscn 25112 | The scalar ring of a subcomplex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ) | ||
| Theorem | clmsub 25113 | Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) → (𝐴 − 𝐵) = (𝐴(-g‘𝐹)𝐵)) | ||
| Theorem | clmneg 25114 | Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → -𝐴 = ((invg‘𝐹)‘𝐴)) | ||
| Theorem | clmneg1 25115 | Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → -1 ∈ 𝐾) | ||
| Theorem | clmabs 25116 | Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → (abs‘𝐴) = ((norm‘𝐹)‘𝐴)) | ||
| Theorem | clmacl 25117 | Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | ||
| Theorem | clmmcl 25118 | Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾) | ||
| Theorem | clmsubcl 25119 | Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 − 𝑌) ∈ 𝐾) | ||
| Theorem | lmhmclm 25120 | The domain of a linear operator is a subcomplex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ ℂMod ↔ 𝑇 ∈ ℂMod)) | ||
| Theorem | clmvscl 25121 | Closure of scalar product for a subcomplex module. Analogue of lmodvscl 20876. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑄 · 𝑋) ∈ 𝑉) | ||
| Theorem | clmvsass 25122 | Associative law for scalar product. Analogue of lmodvsass 20885. (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 · 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) | ||
| Theorem | clmvscom 25123 | Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008.) (Revised by AV, 7-Oct-2021.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (𝑄 · (𝑅 · 𝑋)) = (𝑅 · (𝑄 · 𝑋))) | ||
| Theorem | clmvsdir 25124 | Distributive law for scalar product (right-distributivity). (lmodvsdir 20884 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 + 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) | ||
| Theorem | clmvsdi 25125 | Distributive law for scalar product (left-distributivity). (lmodvsdi 20883 analog.) (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐴 · (𝑋 + 𝑌)) = ((𝐴 · 𝑋) + (𝐴 · 𝑌))) | ||
| Theorem | clmvs1 25126 | Scalar product with ring unity. (lmodvs1 20888 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (1 · 𝑋) = 𝑋) | ||
| Theorem | clmvs2 25127 | 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 25128 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 20893 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (0 · 𝑋) = 0 ) | ||
| Theorem | clmopfne 25129 | 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 25130* | 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 25131* | 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 25132 | Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 20903 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (-1 · 𝑋) = (𝑁‘𝑋)) | ||
| Theorem | clmvsneg 25133 | Multiplication of a vector by a negated scalar. (lmodvsneg 20904 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = (-𝑅 · 𝑋)) | ||
| Theorem | clmmulg 25134 | The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ ∙ = (.g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵)) | ||
| Theorem | clmsubdir 25135 | Scalar multiplication distributive law for subtraction. (lmodsubdir 20918 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋))) | ||
| Theorem | clmpm1dir 25136 | 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 25137 | Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (-1 · (-1 · 𝐴)) = 𝐴) | ||
| Theorem | clmnegsubdi2 25138 | 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 25139 | 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 25140 | 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 25141 | 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 25142 | Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 20915. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵))) | ||
| Theorem | clmvsubval2 25143 | 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 25144 | 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 25145 | The ℤ-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod) | ||
| Theorem | clmzlmvsca 25146 | The scalar product of a subcomplex module matches the scalar product of the derived ℤ-module, which implies, together with zlmbas 21529 and zlmplusg 21531, that any module over ℤ is structure-equivalent to the canonical ℤ-module ℤMod‘𝐺. (Contributed by Mario Carneiro, 30-Oct-2015.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ ℂMod ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑋)) → (𝐴( ·𝑠 ‘𝐺)𝐵) = (𝐴( ·𝑠 ‘𝑊)𝐵)) | ||
| Theorem | nmoleub2lem 25147* | Lemma for nmoleub2a 25150 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 25148* | Lemma for nmoleub2a 25150 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 25149* | Lemma for nmoleub2a 25150 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 𝐺 = (Scalar‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod)) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → ℚ ⊆ 𝐾) & ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥)𝑂𝑅 → (𝐿‘𝑥) ≤ 𝑅)) & ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥) < 𝑅 → (𝐿‘𝑥)𝑂𝑅)) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥)𝑂𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) | ||
| Theorem | nmoleub2a 25150* | 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 25151* | 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 25152* | 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 25153 | 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 25154 | 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 25155 | 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 25157 and characterized in iscvs 25160. These include rational vector spaces (qcvs 25181), real vector spaces (recvs 25179) and complex vector spaces (cncvs 25178). 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 25145) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 25182), because the ring ZZ is not a division ring (see zringndrg 21479). 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 25156 | Syntax for the class of subcomplex vector spaces. |
| class ℂVec | ||
| Definition | df-cvs 25157 | 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 25158 | A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
| ⊢ (𝜑 → 𝑊 ∈ ℂVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ LVec) | ||
| Theorem | cvsclm 25159 | A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.) |
| ⊢ (𝜑 → 𝑊 ∈ ℂVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ ℂMod) | ||
| Theorem | iscvs 25160 | 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 25161* | 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 25162* | 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 25163* | 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 25164 | 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 25165 | Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) = (𝐴(/r‘𝐹)𝐵)) | ||
| Theorem | cvsdivcl 25166 | 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 25167 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → (𝐴 · 𝑋) = (𝐵 · 𝑌)) ⇒ ⊢ (𝜑 → 𝑋 = ((𝐵 / 𝐴) · 𝑌)) | ||
| Theorem | cvsdiveqd 25168 | An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑋 = ((𝐴 / 𝐵) · 𝑌)) ⇒ ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = 𝑌) | ||
| Theorem | cnlmodlem1 25169 | Lemma 1 for cnlmod 25173. (Contributed by AV, 20-Sep-2021.) |
| ⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (Base‘𝑊) = ℂ | ||
| Theorem | cnlmodlem2 25170 | Lemma 2 for cnlmod 25173. (Contributed by AV, 20-Sep-2021.) |
| ⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (+g‘𝑊) = + | ||
| Theorem | cnlmodlem3 25171 | Lemma 3 for cnlmod 25173. (Contributed by AV, 20-Sep-2021.) |
| ⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (Scalar‘𝑊) = ℂfld | ||
| Theorem | cnlmod4 25172 | Lemma 4 for cnlmod 25173. (Contributed by AV, 20-Sep-2021.) |
| ⊢ 𝑊 = ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ∪ {〈(Scalar‘ndx), ℂfld〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( ·𝑠 ‘𝑊) = · | ||
| Theorem | cnlmod 25173 | 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 25174 | 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 25175 | 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 25176 | 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 25177 | 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 25178 | 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 25179 | 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.) (Proof shortened by SN, 23-Nov-2024.) |
| ⊢ 𝑅 = (ringLMod‘ℝfld) ⇒ ⊢ 𝑅 ∈ ℂVec | ||
| Theorem | recvsOLD 25180 | Obsolete version of recvs 25179 as of 23-Nov-2024. (Contributed by AV, 22-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑅 = (ringLMod‘ℝfld) ⇒ ⊢ 𝑅 ∈ ℂVec | ||
| Theorem | qcvs 25181 | 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 25182 | 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 25183. 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 25183* | 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 25184* | 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 25185* | 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 25186 | 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 25187 | 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 25188 | 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 25189 | 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 25190 | 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 25191 | 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 25192 | 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 25193 | 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 25194) . (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.) |
| ⊢ 𝐶 = (ringLMod‘ℂfld) ⇒ ⊢ 𝐶 ∈ (NrmVec ∩ ℂVec) | ||
| Theorem | cnnm 25194 | 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 25195 | 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 25196 | The metric induced on the complex numbers. cnmet 24792 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 21376 and also cnmet 24792. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.) |
| ⊢ 𝑇 = (ℂfld toNrmGrp abs) ⇒ ⊢ (dist‘𝑇) = (abs ∘ − ) | ||
| Theorem | cnncvsaddassdemo 25197 | Derive the associative law for complex number addition addass 11242 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 25198 | Derive the associative law for complex number multiplication mulass 11243 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 25199 | Derive the absolute value of a negative complex number absneg 15316 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 25200 | Extend class notation with the class of subcomplex pre-Hilbert spaces. |
| class ℂPreHil | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |