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	pcorevcl 25001*	Closure for a reversed path. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    ⇒   ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺 ∈ (II Cn 𝐽) ∧ (𝐺‘0) = (𝐹‘1) ∧ (𝐺‘1) = (𝐹‘0)))
Theorem	pcorevlem 25002*	Lemma for pcorev 25003. Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)})    &   ⊢ 𝐻 = (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))))))    ⇒   ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐻 ∈ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ∧ (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃))
Theorem	pcorev 25003*	Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)})    ⇒   ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃)
Theorem	pcorev2 25004*	Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)})    ⇒   ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃)
Theorem	pcophtb 25005*	The path homotopy equivalence relation on two paths 𝐹, 𝐺 with the same start and end point can be written in terms of the loop 𝐹 − 𝐺 formed by concatenating 𝐹 with the inverse of 𝐺. Thus, all the homotopy information in ≃ph‘𝐽 is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐻 = (𝑥 ∈ (0[,]1) ↦ (𝐺‘(1 − 𝑥)))    &   ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)})    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐺‘1))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃 ↔ 𝐹( ≃ph‘𝐽)𝐺))
Theorem	om1val 25006*	The definition of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)})    &   ⊢ (𝜑 → + = (*𝑝‘𝐽))    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↑ko II))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑂 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐾⟩})
Theorem	om1bas 25007*	The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)})
Theorem	om1elbas 25008	Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌 ∧ (𝐹‘1) = 𝑌)))
Theorem	om1addcl 25009	Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    &   ⊢ (𝜑 → 𝐻 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻(*𝑝‘𝐽)𝐾) ∈ 𝐵)
Theorem	om1plusg 25010	The group operation (which isn't much more than a magma) of the loop space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (*𝑝‘𝐽) = (+g‘𝑂))
Theorem	om1tset 25011	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐽 ↑ko II) = (TopSet‘𝑂))
Theorem	om1opn 25012	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝐾 = (TopOpen‘𝑂)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐾 = ((𝐽 ↑ko II) ↾t 𝐵))
Theorem	pi1val 25013	The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    ⇒   ⊢ (𝜑 → 𝐺 = (𝑂 /s ( ≃ph‘𝐽)))
Theorem	pi1bas 25014	The base set of the fundamental group of a topological space at a given base point. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐵 = (𝐾 / ( ≃ph‘𝐽)))
Theorem	pi1blem 25015	Lemma for pi1buni 25016. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽)))
Theorem	pi1buni 25016	Another way to write the loop space base in terms of the base of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → ∪ 𝐵 = 𝐾)
Theorem	pi1bas2 25017	The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽)))
Theorem	pi1eluni 25018	Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐹 ∈ ∪ 𝐵 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌 ∧ (𝐹‘1) = 𝑌)))
Theorem	pi1bas3 25019	The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅))
Theorem	pi1cpbl 25020	The group operation, loop concatenation, is compatible with homotopy equivalence. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ + = (+g‘𝑂)    ⇒   ⊢ (𝜑 → ((𝑀𝑅𝑁 ∧ 𝑃𝑅𝑄) → (𝑀 + 𝑃)𝑅(𝑁 + 𝑄)))
Theorem	elpi1 25021*	The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ ∃𝑓 ∈ (II Cn 𝐽)(((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌) ∧ 𝐹 = [𝑓]( ≃ph‘𝐽))))
Theorem	elpi1i 25022	The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘0) = 𝑌)    &   ⊢ (𝜑 → (𝐹‘1) = 𝑌)    ⇒   ⊢ (𝜑 → [𝐹]( ≃ph‘𝐽) ∈ 𝐵)
Theorem	pi1addf 25023	The group operation of π1 is a binary operation. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐵)
Theorem	pi1addval 25024	The concatenation of two path-homotopy classes in the fundamental group. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ∪ 𝐵)    ⇒   ⊢ (𝜑 → ([𝑀]( ≃ph‘𝐽) + [𝑁]( ≃ph‘𝐽)) = [(𝑀(*𝑝‘𝐽)𝑁)]( ≃ph‘𝐽))
Theorem	pi1grplem 25025	Lemma for pi1grp 25026. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Aug-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 0 = ((0[,]1) × {𝑌})    ⇒   ⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ]( ≃ph‘𝐽) = (0g‘𝐺)))
Theorem	pi1grp 25026	The fundamental group is a group. Proposition 1.3 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) (Revised by Mario Carneiro, 10-Aug-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → 𝐺 ∈ Grp)
Theorem	pi1id 25027	The identity element of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ 0 = ((0[,]1) × {𝑌})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → [ 0 ]( ≃ph‘𝐽) = (0g‘𝐺))
Theorem	pi1inv 25028*	An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘0) = 𝑌)    &   ⊢ (𝜑 → (𝐹‘1) = 𝑌)    &   ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    ⇒   ⊢ (𝜑 → (𝑁‘[𝐹]( ≃ph‘𝐽)) = [𝐼]( ≃ph‘𝐽))
Theorem	pi1xfrf 25029*	Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑃 = (𝐽 π1 (𝐹‘0))    &   ⊢ 𝑄 = (𝐽 π1 (𝐹‘1))    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐼‘0))    &   ⊢ (𝜑 → (𝐼‘1) = (𝐹‘0))    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶(Base‘𝑄))
Theorem	pi1xfrval 25030*	The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑃 = (𝐽 π1 (𝐹‘0))    &   ⊢ 𝑄 = (𝐽 π1 (𝐹‘1))    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐼‘0))    &   ⊢ (𝜑 → (𝐼‘1) = (𝐹‘0))    &   ⊢ (𝜑 → 𝐴 ∈ ∪ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘[𝐴]( ≃ph‘𝐽)) = [(𝐼(*𝑝‘𝐽)(𝐴(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽))
Theorem	pi1xfr 25031*	Given a path 𝐹 and its inverse 𝐼 between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑃 = (𝐽 π1 (𝐹‘0))    &   ⊢ 𝑄 = (𝐽 π1 (𝐹‘1))    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄))
Theorem	pi1xfrcnvlem 25032*	Given a path 𝐹 between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑃 = (𝐽 π1 (𝐹‘0))    &   ⊢ 𝑄 = (𝐽 π1 (𝐹‘1))    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝐻 = ran (ℎ ∈ ∪ (Base‘𝑄) ↦ ⟨[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)⟩)    ⇒   ⊢ (𝜑 → ◡𝐺 ⊆ 𝐻)
Theorem	pi1xfrcnv 25033*	Given a path 𝐹 between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑃 = (𝐽 π1 (𝐹‘0))    &   ⊢ 𝑄 = (𝐽 π1 (𝐹‘1))    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝐻 = ran (ℎ ∈ ∪ (Base‘𝑄) ↦ ⟨[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)⟩)    ⇒   ⊢ (𝜑 → (◡𝐺 = 𝐻 ∧ ◡𝐺 ∈ (𝑄 GrpHom 𝑃)))
Theorem	pi1xfrgim 25034*	The mapping 𝐺 between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑃 = (𝐽 π1 (𝐹‘0))    &   ⊢ 𝑄 = (𝐽 π1 (𝐹‘1))    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpIso 𝑄))
Theorem	pi1cof 25035*	Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑃 = (𝐽 π1 𝐴)    &   ⊢ 𝑄 = (𝐾 π1 𝐵)    &   ⊢ 𝑉 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐵)    ⇒   ⊢ (𝜑 → 𝐺:𝑉⟶(Base‘𝑄))
Theorem	pi1coval 25036*	The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑃 = (𝐽 π1 𝐴)    &   ⊢ 𝑄 = (𝐾 π1 𝐵)    &   ⊢ 𝑉 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑇 ∈ ∪ 𝑉) → (𝐺‘[𝑇]( ≃ph‘𝐽)) = [(𝐹 ∘ 𝑇)]( ≃ph‘𝐾))
Theorem	pi1coghm 25037*	The mapping 𝐺 between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑃 = (𝐽 π1 𝐴)    &   ⊢ 𝑄 = (𝐾 π1 𝐵)    &   ⊢ 𝑉 = (Base‘𝑃)    &   ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ ⟨[𝑔]( ≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐵)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄))
12.5  Metric subcomplex vector spaces
12.5.1  Subcomplex modules
Syntax	cclm 25038	Syntax for the class of subcomplex modules.
class ℂMod
Definition	df-clm 25039*	Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers ℂfld, which allows to use the complex addition, multiplication, etc. in theorems about subcomplex modules. Since the field of complex numbers is commutative and so are its subrings (see subrgcrng 20541), left modules over such subrings are the same as right modules, see rmodislmod 20914. Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
Theorem	isclm 25040	A subcomplex module is a left module over a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)))
Theorem	clmsca 25041	The ring of scalars 𝐹 of a subcomplex module is the restriction of the field of complex numbers to the base set of 𝐹. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂMod → 𝐹 = (ℂfld ↾s 𝐾))
Theorem	clmsubrg 25042	The base set of the ring of scalars of a subcomplex module is the base set of a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂMod → 𝐾 ∈ (SubRing‘ℂfld))
Theorem	clmlmod 25043	A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod)
Theorem	clmgrp 25044	A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp)
Theorem	clmabl 25045	A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel)
Theorem	clmring 25046	The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Ring)
Theorem	clmfgrp 25047	The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp)
Theorem	clm0 25048	The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘𝐹))
Theorem	clm1 25049	The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 1 = (1r‘𝐹))
Theorem	clmadd 25050	The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → + = (+g‘𝐹))
Theorem	clmmul 25051	The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → · = (.r‘𝐹))
Theorem	clmcj 25052	The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → ∗ = (*𝑟‘𝐹))
Theorem	isclmi 25053	Reverse direction of isclm 25040. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) → 𝑊 ∈ ℂMod)
Theorem	clmzss 25054	The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂMod → ℤ ⊆ 𝐾)
Theorem	clmsscn 25055	The scalar ring of a subcomplex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ)
Theorem	clmsub 25056	Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) → (𝐴 − 𝐵) = (𝐴(-g‘𝐹)𝐵))
Theorem	clmneg 25057	Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → -𝐴 = ((invg‘𝐹)‘𝐴))
Theorem	clmneg1 25058	Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂMod → -1 ∈ 𝐾)
Theorem	clmabs 25059	Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → (abs‘𝐴) = ((norm‘𝐹)‘𝐴))
Theorem	clmacl 25060	Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾)
Theorem	clmmcl 25061	Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾)
Theorem	clmsubcl 25062	Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 − 𝑌) ∈ 𝐾)
Theorem	lmhmclm 25063	The domain of a linear operator is a subcomplex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ ℂMod ↔ 𝑇 ∈ ℂMod))
Theorem	clmvscl 25064	Closure of scalar product for a subcomplex module. Analogue of lmodvscl 20862. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑄 · 𝑋) ∈ 𝑉)
Theorem	clmvsass 25065	Associative law for scalar product. Analogue of lmodvsass 20871. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 · 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
Theorem	clmvscom 25066	Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008.) (Revised by AV, 7-Oct-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (𝑄 · (𝑅 · 𝑋)) = (𝑅 · (𝑄 · 𝑋)))
Theorem	clmvsdir 25067	Distributive law for scalar product (right-distributivity). (lmodvsdir 20870 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 + 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
Theorem	clmvsdi 25068	Distributive law for scalar product (left-distributivity). (lmodvsdi 20869 analog.) (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐴 · (𝑋 + 𝑌)) = ((𝐴 · 𝑋) + (𝐴 · 𝑌)))
Theorem	clmvs1 25069	Scalar product with ring unity. (lmodvs1 20874 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (1 · 𝑋) = 𝑋)
Theorem	clmvs2 25070	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 25071	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 20879 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (0 · 𝑋) = 0 )
Theorem	clmopfne 25072	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 25073*	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 25074*	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 25075	Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 20889 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (-1 · 𝑋) = (𝑁‘𝑋))
Theorem	clmvsneg 25076	Multiplication of a vector by a negated scalar. (lmodvsneg 20890 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = (-𝑅 · 𝑋))
Theorem	clmmulg 25077	The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ∙ = (.g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵))
Theorem	clmsubdir 25078	Scalar multiplication distributive law for subtraction. (lmodsubdir 20904 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋)))
Theorem	clmpm1dir 25079	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 25080	Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (-1 · (-1 · 𝐴)) = 𝐴)
Theorem	clmnegsubdi2 25081	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 25082	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 25083	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 25084	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 25085	Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 20901. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵)))
Theorem	clmvsubval2 25086	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 25087	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 25088	The ℤ-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod)
Theorem	clmzlmvsca 25089	The scalar product of a subcomplex module matches the scalar product of the derived ℤ-module, which implies, together with zlmbas 21505 and zlmplusg 21506, that any module over ℤ is structure-equivalent to the canonical ℤ-module ℤMod‘𝐺. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ℂMod ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑋)) → (𝐴( ·𝑠 ‘𝐺)𝐵) = (𝐴( ·𝑠 ‘𝑊)𝐵))
Theorem	nmoleub2lem 25090*	Lemma for nmoleub2a 25093 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 25091*	Lemma for nmoleub2a 25093 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 25092*	Lemma for nmoleub2a 25093 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 𝐺 = (Scalar‘𝑆)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩ ℂMod))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → ℚ ⊆ 𝐾)    &   ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥)𝑂𝑅 → (𝐿‘𝑥) ≤ 𝑅))    &   ⊢ (((𝐿‘𝑥) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((𝐿‘𝑥) < 𝑅 → (𝐿‘𝑥)𝑂𝑅))    ⇒   ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 ((𝐿‘𝑥)𝑂𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)))
Theorem	nmoleub2a 25093*	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 25094*	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 25095*	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 25096	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 25097	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 25098	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 25100 and characterized in iscvs 25103. These include rational vector spaces (qcvs 25123), real vector spaces (recvs 25122) and complex vector spaces (cncvs 25121). 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 25088) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 25124), because the ring ZZ is not a division ring (see zringndrg 21456). 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 25099	Syntax for the class of subcomplex vector spaces.
class ℂVec
Definition	df-cvs 25100	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)