P. 230 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clmmulg 22901	The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ∙ = (.g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵))
Theorem	clmsubdir 22902	Scalar multiplication distributive law for subtraction. (lmodsubdir 18921 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋)))
Theorem	clmpm1dir 22903	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 22904	Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (-1 · (-1 · 𝐴)) = 𝐴)
Theorem	clmnegsubdi2 22905	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 22906	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 22907	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 22908	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 22909	Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 18918. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵)))
Theorem	clmvsubval2 22910	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 22911	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 22912	The ℤ-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod)
Theorem	clmzlmvsca 22913	The scalar product of a subcomplex module matches the scalar product of the derived ℤ-module, which implies, together with zlmbas 19866 and zlmplusg 19867, that any module over ℤ is structure-equivalent to the canonical ℤ-module ℤMod‘𝐺. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ℂMod ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑋)) → (𝐴( ·𝑠 ‘𝐺)𝐵) = (𝐴( ·𝑠 ‘𝑊)𝐵))
Theorem	nmoleub2lem 22914*	Lemma for nmoleub2a 22917 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 22915*	Lemma for nmoleub2a 22917 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 22916*	Lemma for nmoleub2a 22917 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 𝐺 = (Scalar‘𝑆)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → ℚ ⊆ 𝐾)    &   ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥)𝑂𝑅 → (𝐿‘𝑥) ≤ 𝑅))    &   ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥) < 𝑅 → (𝐿‘𝑥)𝑂𝑅))    ⇒   ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥)𝑂𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)))
Theorem	nmoleub2a 22917*	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 22918*	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 22919*	The operator norm is the supremum of the value of a linear operator on the closed unit sphere. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 𝐺 = (Scalar‘𝑆)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → ℝ ⊆ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥) = 𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)))
Theorem	nmhmcn 22920	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 22921	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 22922	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 22924 and characterized in iscvs 22927. These include rational vector spaces (qcvs 22947), real vector spaces (recvs 22946) and complex vector spaces (cncvs 22945). 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 22912) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 22948), because the ring ZZ is not a division ring (see zringndrg 19838). 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 22923	Syntax for the class of subcomplex vector spaces.
class ℂVec
Definition	df-cvs 22924	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 22925	A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ (𝜑 → 𝑊 ∈ ℂVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ LVec)
Theorem	cvsclm 22926	A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ (𝜑 → 𝑊 ∈ ℂVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ ℂMod)
Theorem	iscvs 22927	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 22928*	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 22929*	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 22930*	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 22931	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 22932	Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) = (𝐴(/r‘𝐹)𝐵))
Theorem	cvsdivcl 22933	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 22934	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → (𝐴 · 𝑋) = (𝐵 · 𝑌))    ⇒   ⊢ (𝜑 → 𝑋 = ((𝐵 / 𝐴) · 𝑌))
Theorem	cvsdiveqd 22935	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝑋 = ((𝐴 / 𝐵) · 𝑌))    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = 𝑌)
Theorem	cnlmodlem1 22936	Lemma 1 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (Base‘𝑊) = ℂ
Theorem	cnlmodlem2 22937	Lemma 2 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (+g‘𝑊) = +
Theorem	cnlmodlem3 22938	Lemma 3 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (Scalar‘𝑊) = ℂfld
Theorem	cnlmod4 22939	Lemma 4 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( ·𝑠 ‘𝑊) = ·
Theorem	cnlmod 22940	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 22941	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 22942	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 22943	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 22944	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 22945	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 22946	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 22947	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 22948	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 22949. 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 22949*	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 22950*	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 22951*	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 22952	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 22953	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 22954	The norm of the negative of a vector. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 8-Oct-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ 𝐴 ∈ 𝑉) → (𝑁‘(-1 · 𝐴)) = (𝑁‘𝐴))
Theorem	ncvsdif 22955	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 22956	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 22957	From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (Revised by AV, 8-Oct-2021.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝐺)    &   ⊢ 𝐹 = (Scalar‘𝐺)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝐺 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝑁‘((1 / (𝑁‘𝐴)) · 𝐴)) = 1)
Theorem	cnrnvc 22958	The set of complex numbers (as a subring of itself) is a normed vector space over itself. The vector operation is +, and the scalar product is ·, and the norm function is abs. (Contributed by AV, 9-Oct-2021.)
⊢ 𝐶 = (ringLMod‘ℂfld)    ⇒   ⊢ 𝐶 ∈ NrmVec
Theorem	cnncvs 22959	The set of complex numbers (as a subring of itself) is a normed subcomplex vector space. The vector operation is +, and the scalar product is ·, and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.)
⊢ 𝐶 = (ringLMod‘ℂfld)    ⇒   ⊢ 𝐶 ∈ (NrmVec ∩ ℂVec)
Theorem	cnnm 22960	The norm operation of the normed subcomplex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.)
⊢ 𝐶 = (ringLMod‘ℂfld)    ⇒   ⊢ (norm‘𝐶) = abs
Theorem	ncvspds 22961	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 22962	The metric induced on the complex numbers. cnmet 22575 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 19756 and also cnmet 22575. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.)
⊢ 𝑇 = (ℂfld toNrmGrp abs)    ⇒   ⊢ (dist‘𝑇) = (abs ∘ − )
Theorem	cnncvsaddassdemo 22963	Derive the associative law for complex number addition addass 10023 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 22964	Derive the associative law for complex number multiplication mulass 10024 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 22965	Derive the absolute value of a negative complex number absneg 14017 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 space
Syntax	ccph 22966	Extend class notation with a class of subcomplex pre-Hilbert spaces.
class ℂPreHil
Syntax	ctch 22967	Function to put a norm on a Hilbert space.
class toℂHil
Definition	df-cph 22968*	Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a quadratically closed subfield of ℂfld, we have enough structure to define a norm, with the associated connection to a metric and topology. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))}
Definition	df-tch 22969*	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ℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))
Theorem	iscph 22970*	A subcomplex pre-Hilbert space is a pre-Hilbert space over a quadratically closed subfield of the field of complex numbers, with a norm defined. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld ↾s 𝐾)) ∧ (√ “ (𝐾 ∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))))
Theorem	cphphl 22971	A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
Theorem	cphnlm 22972	A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod)
Theorem	cphngp 22973	A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
Theorem	cphlmod 22974	A subcomplex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
Theorem	cphlvec 22975	A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LVec)
Theorem	cphnvc 22976	A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmVec)
Theorem	cphsubrglem 22977	Lemma for cphsubrg 22980. (Contributed by Mario Carneiro, 9-Oct-2015.)
⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴))    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → (𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 = (𝐴 ∩ ℂ) ∧ 𝐾 ∈ (SubRing‘ℂfld)))
Theorem	cphreccllem 22978	Lemma for cphreccl 22981. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴))    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0) → (1 / 𝑋) ∈ 𝐾)
Theorem	cphsca 22979	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 22980	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 22981	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 22982	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 22983	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 22984	The scalar field of a subcomplex pre-Hilbert space is closed under square roots of positive reals (i.e. it is quadratically closed relative to ℝ). (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) → (√‘𝐴) ∈ 𝐾)
Theorem	cphabscl 22985	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 22986	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 22987	If the scalar field contains i, it is completely closed under square roots (i.e. it is quadratically closed). (Contributed by Mario Carneiro, 11-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾) → (√‘𝐴) ∈ 𝐾)
Theorem	cphqss 22988	The scalar field of a subcomplex pre-Hilbert space contains all rational numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂPreHil → ℚ ⊆ 𝐾)
Theorem	cphclm 22989	A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
Theorem	cphnmvs 22990	Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((abs‘𝑋) · (𝑁‘𝑌)))
Theorem	cphipcl 22991	An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ ℂ)
Theorem	cphnmfval 22992*	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 22993	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 22994	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 22995	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 → 𝑁:𝑉⟶𝐾)
Theorem	cphnmcl 22996	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 ∧ 𝐴 ∈ 𝑉) → (𝑁‘𝐴) ∈ 𝐾)
Theorem	reipcl 22997	An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 𝐴) ∈ ℝ)
Theorem	ipge0 22998	The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → 0 ≤ (𝐴 , 𝐴))
Theorem	cphipcj 22999	Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj 19979. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∗‘(𝐴 , 𝐵)) = (𝐵 , 𝐴))
Theorem	cphipipcj 23000	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (Revised by AV, 19-Oct-2021.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) · (𝐵 , 𝐴)) = ((abs‘(𝐴 , 𝐵))↑2))