P. 252 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25101-25200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cvslvec 25101	A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ (𝜑 → 𝑊 ∈ ℂVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ LVec)
Theorem	cvsclm 25102	A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ (𝜑 → 𝑊 ∈ ℂVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ ℂMod)
Theorem	iscvs 25103	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 25104*	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 25105*	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 25106*	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 25107	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 25108	Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂVec ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) = (𝐴(/r‘𝐹)𝐵))
Theorem	cvsdivcl 25109	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 25110	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → (𝐴 · 𝑋) = (𝐵 · 𝑌))    ⇒   ⊢ (𝜑 → 𝑋 = ((𝐵 / 𝐴) · 𝑌))
Theorem	cvsdiveqd 25111	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝑋 = ((𝐴 / 𝐵) · 𝑌))    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = 𝑌)
Theorem	cnlmodlem1 25112	Lemma 1 for cnlmod 25116. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (Base‘𝑊) = ℂ
Theorem	cnlmodlem2 25113	Lemma 2 for cnlmod 25116. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (+g‘𝑊) = +
Theorem	cnlmodlem3 25114	Lemma 3 for cnlmod 25116. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (Scalar‘𝑊) = ℂfld
Theorem	cnlmod4 25115	Lemma 4 for cnlmod 25116. (Contributed by AV, 20-Sep-2021.)
⊢ 𝑊 = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ∪ {⟨(Scalar‘ndx), ℂfld⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( ·𝑠 ‘𝑊) = ·
Theorem	cnlmod 25116	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 25117	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 25118	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 25119	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 25120	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 25121	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 25122	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 25123	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 25124	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 25125. 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 25125*	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 25126*	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 25127*	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 25128	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 25129	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 25130	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 25131	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 25132	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 25133	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 25134	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 25135	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 25136) . (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.)
⊢ 𝐶 = (ringLMod‘ℂfld)    ⇒   ⊢ 𝐶 ∈ (NrmVec ∩ ℂVec)
Theorem	cnnm 25136	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 25137	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 25138	The metric induced on the complex numbers. cnmet 24745 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 21354 and also cnmet 24745. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.)
⊢ 𝑇 = (ℂfld toNrmGrp abs)    ⇒   ⊢ (dist‘𝑇) = (abs ∘ − )
Theorem	cnncvsaddassdemo 25139	Derive the associative law for complex number addition addass 11114 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 25140	Derive the associative law for complex number multiplication mulass 11115 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 25141	Derive the absolute value of a negative complex number absneg 15228 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 25142	Extend class notation with the class of subcomplex pre-Hilbert spaces.
class ℂPreHil
Syntax	ctcph 25143	Function to put a norm on a pre-Hilbert space.
class toℂPreHil
Definition	df-cph 25144*	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 25145*	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 25213). (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))
Theorem	iscph 25146*	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 25147	A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
Theorem	cphnlm 25148	A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod)
Theorem	cphngp 25149	A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
Theorem	cphlmod 25150	A subcomplex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
Theorem	cphlvec 25151	A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LVec)
Theorem	cphnvc 25152	A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmVec)
Theorem	cphsubrglem 25153	Lemma for cphsubrg 25156. (Contributed by Mario Carneiro, 9-Oct-2015.)
⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴))    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → (𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 = (𝐴 ∩ ℂ) ∧ 𝐾 ∈ (SubRing‘ℂfld)))
Theorem	cphreccllem 25154	Lemma for cphreccl 25157. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐴))    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0) → (1 / 𝑋) ∈ 𝐾)
Theorem	cphsca 25155	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 25156	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 25157	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 25158	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 25159	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 25160	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 25161	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 25162	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 25163	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 25164	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 25165	A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
Theorem	cphnmvs 25166	Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((abs‘𝑋) · (𝑁‘𝑌)))
Theorem	cphipcl 25167	An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ ℂ)
Theorem	cphnmfval 25168*	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 25169	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 25170	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 25171	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 25172	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 25173	An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 𝐴) ∈ ℝ)
Theorem	ipge0 25174	The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → 0 ≤ (𝐴 , 𝐴))
Theorem	cphipcj 25175	Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj 21622. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∗‘(𝐴 , 𝐵)) = (𝐵 , 𝐴))
Theorem	cphipipcj 25176	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (Revised by AV, 19-Oct-2021.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) · (𝐵 , 𝐴)) = ((abs‘(𝐴 , 𝐵))↑2))
Theorem	cphorthcom 25177	Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 21623. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) = 0 ↔ (𝐵 , 𝐴) = 0))
Theorem	cphip0l 25178	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 21624. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ( 0 , 𝐴) = 0)
Theorem	cphip0r 25179	Inner product with a zero second argument. Complex version of ip0r 21625. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 0 ) = 0)
Theorem	cphipeq0 25180	The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. Complex version of ipeq0 21626. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ((𝐴 , 𝐴) = 0 ↔ 𝐴 = 0 ))
Theorem	cphdir 25181	Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 21627. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 + 𝐵) , 𝐶) = ((𝐴 , 𝐶) + (𝐵 , 𝐶)))
Theorem	cphdi 25182	Distributive law for inner product (left-distributivity). Complex version of ipdi 21628. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 + 𝐶)) = ((𝐴 , 𝐵) + (𝐴 , 𝐶)))
Theorem	cph2di 25183	Distributive law for inner product. Complex version of ip2di 21629. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) , (𝐶 + 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) + ((𝐴 , 𝐷) + (𝐵 , 𝐶))))
Theorem	cphsubdir 25184	Distributive law for inner product subtraction. Complex version of ipsubdir 21630. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) , 𝐶) = ((𝐴 , 𝐶) − (𝐵 , 𝐶)))
Theorem	cphsubdi 25185	Distributive law for inner product subtraction. Complex version of ipsubdi 21631. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 − 𝐶)) = ((𝐴 , 𝐵) − (𝐴 , 𝐶)))
Theorem	cph2subdi 25186	Distributive law for inner product subtraction. Complex version of ip2subdi 21632. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) − ((𝐴 , 𝐷) + (𝐵 , 𝐶))))
Theorem	cphass 25187	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 21633, his5 31177. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 · 𝐵) , 𝐶) = (𝐴 · (𝐵 , 𝐶)))
Theorem	cphassr 25188	"Associative" law for second argument of inner product (compare cphass 25187). See ipassr 21634, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 , (𝐴 · 𝐶)) = ((∗‘𝐴) · (𝐵 , 𝐶)))
Theorem	cph2ass 25189	Move scalar multiplication to outside of inner product. See his35 31179. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 · 𝐶) , (𝐵 · 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 , 𝐷)))
Theorem	cphassi 25190	Associative law for the first argument of an inner product with scalar _𝑖. (Contributed by AV, 17-Oct-2021.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) = (i · (𝐵 , 𝐴)))
Theorem	cphassir 25191	"Associative" law for the second argument of an inner product with scalar _𝑖. (Contributed by AV, 17-Oct-2021.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) = (-i · (𝐴 , 𝐵)))
Theorem	cphpyth 25192	The pythagorean theorem for a subcomplex pre-Hilbert space. The square of the norm of the sum of two orthogonal vectors (i.e., whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008.) (Revised by SN, 22-Sep-2024.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ (𝐴 , 𝐵) = 0) → ((𝑁‘(𝐴 + 𝐵))↑2) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))
Theorem	tcphex 25193*	Lemma for tcphbas 25195 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))) ∈ V
Theorem	tcphval 25194*	Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ 𝐺 = (𝑊 toNrmGrp (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))
Theorem	tcphbas 25195	The base set of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ 𝑉 = (Base‘𝐺)
Theorem	tchplusg 25196	The addition operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ + = (+g‘𝐺)
Theorem	tcphsub 25197	The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ − = (-g‘𝐺)
Theorem	tcphmulr 25198	The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ · = (.r‘𝑊)    ⇒   ⊢ · = (.r‘𝐺)
Theorem	tcphsca 25199	The scalar field of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ 𝐹 = (Scalar‘𝐺)
Theorem	tcphvsca 25200	The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ · = ( ·𝑠 ‘𝐺)