P. 251 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25001-25100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clmvs2 25001	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 25002	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 20808 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (0 · 𝑋) = 0 )
Theorem	clmopfne 25003	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 25004*	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 25005*	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 25006	Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 20818 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (-1 · 𝑋) = (𝑁‘𝑋))
Theorem	clmvsneg 25007	Multiplication of a vector by a negated scalar. (lmodvsneg 20819 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = (-𝑅 · 𝑋))
Theorem	clmmulg 25008	The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ∙ = (.g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵))
Theorem	clmsubdir 25009	Scalar multiplication distributive law for subtraction. (lmodsubdir 20833 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋)))
Theorem	clmpm1dir 25010	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 25011	Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (-1 · (-1 · 𝐴)) = 𝐴)
Theorem	clmnegsubdi2 25012	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 25013	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 25014	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 25015	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 25016	Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 20830. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵)))
Theorem	clmvsubval2 25017	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 25018	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 25019	The ℤ-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod)
Theorem	clmzlmvsca 25020	The scalar product of a subcomplex module matches the scalar product of the derived ℤ-module, which implies, together with zlmbas 21434 and zlmplusg 21435, that any module over ℤ is structure-equivalent to the canonical ℤ-module ℤMod‘𝐺. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ℂMod ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑋)) → (𝐴( ·𝑠 ‘𝐺)𝐵) = (𝐴( ·𝑠 ‘𝑊)𝐵))
Theorem	nmoleub2lem 25021*	Lemma for nmoleub2a 25024 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 25022*	Lemma for nmoleub2a 25024 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 25023*	Lemma for nmoleub2a 25024 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 𝐺 = (Scalar‘𝑆)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → ℚ ⊆ 𝐾)    &   ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥)𝑂𝑅 → (𝐿‘𝑥) ≤ 𝑅))    &   ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥) < 𝑅 → (𝐿‘𝑥)𝑂𝑅))    ⇒   ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥)𝑂𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)))
Theorem	nmoleub2a 25024*	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 25025*	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 25026*	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 25027	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 25028	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 25029	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↑𝑁) · 𝐵) ∈ 𝑋)
12.5.2  Subcomplex vector spaces 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 25031 and characterized in iscvs 25034. These include rational vector spaces (qcvs 25054), real vector spaces (recvs 25053) and complex vector spaces (cncvs 25052). 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 25019) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 25055), because the ring ZZ is not a division ring (see zringndrg 21385). 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 25030	Syntax for the class of subcomplex vector spaces.
class ℂVec
Definition	df-cvs 25031	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 25032	A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ (𝜑 → 𝑊 ∈ ℂVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ LVec)
Theorem	cvsclm 25033	A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ (𝜑 → 𝑊 ∈ ℂVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ ℂMod)
Theorem	iscvs 25034	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 25035*	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 25036*	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 25037*	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 25038	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 25039	Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) = (𝐴(/r‘𝐹)𝐵))
Theorem	cvsdivcl 25040	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 25041	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → (𝐴 · 𝑋) = (𝐵 · 𝑌))    ⇒   ⊢ (𝜑 → 𝑋 = ((𝐵 / 𝐴) · 𝑌))
Theorem	cvsdiveqd 25042	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝑋 = ((𝐴 / 𝐵) · 𝑌))    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = 𝑌)
Theorem	cnlmodlem1 25043	Lemma 1 for cnlmod 25047. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (Base‘𝑊) = ℂ
Theorem	cnlmodlem2 25044	Lemma 2 for cnlmod 25047. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (+g‘𝑊) = +
Theorem	cnlmodlem3 25045	Lemma 3 for cnlmod 25047. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (Scalar‘𝑊) = ℂfld
Theorem	cnlmod4 25046	Lemma 4 for cnlmod 25047. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( ·𝑠 ‘𝑊) = ·
Theorem	cnlmod 25047	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 25048	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 25049	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 25050	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 25051	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 25052	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 25053	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	qcvs 25054	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 25055	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)
12.5.3  Normed subcomplex vector spaces 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 25056. 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 25056*	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 25057*	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 25058*	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 25059	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 25060	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 25061	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 25062	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 25063	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 25064	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 25065	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 25066	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 25067) . (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.)
⊢ 𝐶 = (ringLMod‘ℂfld)    ⇒   ⊢ 𝐶 ∈ (NrmVec ∩ ℂVec)
Theorem	cnnm 25067	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 25068	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 25069	The metric induced on the complex numbers. cnmet 24666 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 21283 and also cnmet 24666. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.)
⊢ 𝑇 = (ℂfld toNrmGrp abs)    ⇒   ⊢ (dist‘𝑇) = (abs ∘ − )
Theorem	cnncvsaddassdemo 25070	Derive the associative law for complex number addition addass 11162 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 25071	Derive the associative law for complex number multiplication mulass 11163 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 25072	Derive the absolute value of a negative complex number absneg 15250 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‘𝐴))
12.5.4  Subcomplex pre-Hilbert spaces
Syntax	ccph 25073	Extend class notation with the class of subcomplex pre-Hilbert spaces.
class ℂPreHil
Syntax	ctcph 25074	Function to put a norm on a pre-Hilbert space.
class toℂPreHil
Definition	df-cph 25075*	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 25076*	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 (see tcphcph 25144). (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))
Theorem	iscph 25077*	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 25078	A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
Theorem	cphnlm 25079	A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod)
Theorem	cphngp 25080	A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
Theorem	cphlmod 25081	A subcomplex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
Theorem	cphlvec 25082	A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LVec)
Theorem	cphnvc 25083	A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmVec)
Theorem	cphsubrglem 25084	Lemma for cphsubrg 25087. (Contributed by Mario Carneiro, 9-Oct-2015.)
⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴))    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → (𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 = (𝐴 ∩ ℂ) ∧ 𝐾 ∈ (SubRing‘ℂfld)))
Theorem	cphreccllem 25085	Lemma for cphreccl 25088. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴))    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0) → (1 / 𝑋) ∈ 𝐾)
Theorem	cphsca 25086	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 25087	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 25088	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 25089	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 25090	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 25091	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 25092	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 25093	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 25094	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 25095	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 25096	A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
Theorem	cphnmvs 25097	Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((abs‘𝑋) · (𝑁‘𝑌)))
Theorem	cphipcl 25098	An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ ℂ)
Theorem	cphnmfval 25099*	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 25100	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 ∧ 𝐴 ∈ 𝑉) → (𝑁‘𝐴) = (√‘(𝐴 , 𝐴)))