P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	phtpyhtpy 24901	A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺))
Theorem	phtpycn 24902	A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ ((II ×t II) Cn 𝐽))
Theorem	phtpyi 24903	Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → ((0𝐻𝐴) = (𝐹‘0) ∧ (1𝐻𝐴) = (𝐹‘1)))
Theorem	phtpy01 24904	Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))    ⇒   ⊢ (𝜑 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1)))
Theorem	isphtpyd 24905*	Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘0))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘1))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))
Theorem	isphtpy2d 24906*	Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐻 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻0) = (𝐹‘𝑠))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻1) = (𝐺‘𝑠))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘0))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘1))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))
Theorem	phtpycom 24907*	Given a homotopy from 𝐹 to 𝐺, produce a homotopy from 𝐺 to 𝐹. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥𝐻(1 − 𝑦)))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝐺(PHtpy‘𝐽)𝐹))
Theorem	phtpyid 24908*	A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐹(PHtpy‘𝐽)𝐹))
Theorem	phtpyco2 24909	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺)))
Theorem	phtpycc 24910*	Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
⊢ 𝑀 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐾(2 · 𝑦)), (𝑥𝐿((2 · 𝑦) − 1))))    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ (𝐹(PHtpy‘𝐽)𝐺))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐺(PHtpy‘𝐽)𝐻))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻))
Definition	df-phtpc 24911*	Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)
⊢ ≃ph = (𝑥 ∈ Top ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)})
Theorem	phtpcrel 24912	The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.)
⊢ Rel ( ≃ph‘𝐽)
Theorem	isphtpc 24913	The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ (𝐹( ≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))
Theorem	phtpcer 24914	Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof shortened by AV, 1-May-2021.)
⊢ ( ≃ph‘𝐽) Er (II Cn 𝐽)
Theorem	phtpc01 24915	Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝐹( ≃ph‘𝐽)𝐺 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1)))
Theorem	reparphti 24916*	Lemma for reparpht 24918. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) Avoid ax-mulf 11078. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn II))    &   ⊢ (𝜑 → (𝐺‘0) = 0)    &   ⊢ (𝜑 → (𝐺‘1) = 1)    &   ⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))))    ⇒   ⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹))
Theorem	reparphtiOLD 24917*	Obsolete version of reparphti 24916 as of 9-Apr-2025. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn II))    &   ⊢ (𝜑 → (𝐺‘0) = 0)    &   ⊢ (𝜑 → (𝐺‘1) = 1)    &   ⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))))    ⇒   ⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹))
Theorem	reparpht 24918	Reparametrization lemma. The reparametrization of a path by any continuous map 𝐺:II⟶II with 𝐺(0) = 0 and 𝐺(1) = 1 is path-homotopic to the original path. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn II))    &   ⊢ (𝜑 → (𝐺‘0) = 0)    &   ⊢ (𝜑 → (𝐺‘1) = 1)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺)( ≃ph‘𝐽)𝐹)
Theorem	phtpcco2 24919	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺)    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐹)( ≃ph‘𝐾)(𝑃 ∘ 𝐺))
12.4.13  The fundamental group
Syntax	cpco 24920	Extend class notation with the concatenation operation for paths in a topological space.
class *𝑝
Syntax	comi 24921	Extend class notation with the loop space.
class Ω1
Syntax	comn 24922	Extend class notation with the higher loop spaces.
class Ω𝑛
Syntax	cpi1 24923	Extend class notation with the fundamental group.
class π1
Syntax	cpin 24924	Extend class notation with the higher homotopy groups.
class πn
Definition	df-pco 24925*	Define the concatenation of two paths in a topological space 𝐽. For simplicity of definition, we define it on all paths, not just those whose endpoints line up. Definition of [Hatcher] p. 26. Hatcher denotes path concatenation with a square dot; other authors, such as Munkres, use a star. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ *𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
Definition	df-om1 24926*	Define the loop space of a topological space, with a magma structure on it given by concatenation of loops. This structure is not a group, but the operation is compatible with homotopy, which allows the homotopy groups to be defined based on this operation. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ Ω1 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ {⟨(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}⟩, ⟨(+g‘ndx), (*𝑝‘𝑗)⟩, ⟨(TopSet‘ndx), (𝑗 ↑ko II)⟩})
Definition	df-omn 24927*	Define the n-th iterated loop space of a topological space. Unlike Ω1 this is actually a pointed topological space, which is to say a tuple of a topological space (a member of TopSp, not Top) and a point in the space. Higher loop spaces select the constant loop at the point from the lower loop space for the distinguished point. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ Ω𝑛 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), ∪ 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩))
Definition	df-pi1 24928*	Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ π1 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph‘𝑗)))
Definition	df-pin 24929*	Define the n-th homotopy group, which is formed by taking the 𝑛-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the 𝑛-th loop space, which is the 𝑛 − 1-th loop space. For 𝑛 = 0, since this is not well-defined we replace this relation with the path-connectedness relation, so that the 0-th homotopy group is the set of path components of 𝑋. (Since the 0-th loop space does not have a group operation, neither does the 0-th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ πn = (𝑗 ∈ Top, 𝑝 ∈ ∪ 𝑗 ↦ (𝑛 ∈ ℕ0 ↦ ((1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛)) /s if(𝑛 = 0, {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1)))))))))
Theorem	pcofval 24930*	The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof shortened by AV, 2-Mar-2024.)
⊢ (*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
Theorem	pcoval 24931*	The concatenation of two paths. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))))
Theorem	pcovalg 24932	Evaluate the concatenation of two paths. (Contributed by Mario Carneiro, 7-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))))
Theorem	pcoval1 24933	Evaluate the concatenation of two paths on the first half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,](1 / 2))) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = (𝐹‘(2 · 𝑋)))
Theorem	pco0 24934	The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0))
Theorem	pco1 24935	The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1))
Theorem	pcoval2 24936	Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = (𝐺‘((2 · 𝑋) − 1)))
Theorem	pcocn 24937	The concatenation of two paths is a path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))    ⇒   ⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽))
Theorem	copco 24938	The composition of a concatenation of paths with a continuous function. (Contributed by Mario Carneiro, 9-Jul-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹(*𝑝‘𝐽)𝐺)) = ((𝐻 ∘ 𝐹)(*𝑝‘𝐾)(𝐻 ∘ 𝐺)))
Theorem	pcohtpylem 24939*	Lemma for pcohtpy 24940. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))    &   ⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐻)    &   ⊢ (𝜑 → 𝐺( ≃ph‘𝐽)𝐾)    &   ⊢ 𝑃 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)))    &   ⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺(PHtpy‘𝐽)𝐾))    ⇒   ⊢ (𝜑 → 𝑃 ∈ ((𝐹(*𝑝‘𝐽)𝐺)(PHtpy‘𝐽)(𝐻(*𝑝‘𝐽)𝐾)))
Theorem	pcohtpy 24940	Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))    &   ⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐻)    &   ⊢ (𝜑 → 𝐺( ≃ph‘𝐽)𝐾)    ⇒   ⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)(𝐻(*𝑝‘𝐽)𝐾))
Theorem	pcoptcl 24941	A constant function is a path from 𝑌 to itself. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑃 = ((0[,]1) × {𝑌})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = 𝑌 ∧ (𝑃‘1) = 𝑌))
Theorem	pcopt 24942	Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ 𝑃 = ((0[,]1) × {𝑌})    ⇒   ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝐹)
Theorem	pcopt2 24943	Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑃 = ((0[,]1) × {𝑌})    ⇒   ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = 𝑌) → (𝐹(*𝑝‘𝐽)𝑃)( ≃ph‘𝐽)𝐹)
Theorem	pcoass 24944*	Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))    &   ⊢ (𝜑 → (𝐺‘1) = (𝐻‘0))    &   ⊢ 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)))
Theorem	pcorevcl 24945*	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 24946*	Lemma for pcorev 24947. 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 24947*	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 24948*	Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)})    ⇒   ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃)
Theorem	pcophtb 24949*	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 24950*	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 24951*	The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)})
Theorem	om1elbas 24952	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 24953	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 24954	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 24955	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐽 ↑ko II) = (TopSet‘𝑂))
Theorem	om1opn 24956	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝐾 = (TopOpen‘𝑂)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐾 = ((𝐽 ↑ko II) ↾t 𝐵))
Theorem	pi1val 24957	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 24958	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 24959	Lemma for pi1buni 24960. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽)))
Theorem	pi1buni 24960	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 24961	The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽)))
Theorem	pi1eluni 24962	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 24963	The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅))
Theorem	pi1cpbl 24964	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 24965*	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 24966	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 24967	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 24968	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 24969	Lemma for pi1grp 24970. (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 24970	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 24971	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 24972*	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 24973*	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 24974*	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 24975*	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 24976*	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 24977*	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 24978*	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 24979*	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 24980*	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 24981*	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 24982	Syntax for the class of subcomplex modules.
class ℂMod
Definition	df-clm 24983*	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 20483), left modules over such subrings are the same as right modules, see rmodislmod 20856. 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 24984	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 24985	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 24986	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 24987	A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod)
Theorem	clmgrp 24988	A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp)
Theorem	clmabl 24989	A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel)
Theorem	clmring 24990	The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Ring)
Theorem	clmfgrp 24991	The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp)
Theorem	clm0 24992	The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘𝐹))
Theorem	clm1 24993	The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → 1 = (1r‘𝐹))
Theorem	clmadd 24994	The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → + = (+g‘𝐹))
Theorem	clmmul 24995	The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → · = (.r‘𝐹))
Theorem	clmcj 24996	The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂMod → ∗ = (*𝑟‘𝐹))
Theorem	isclmi 24997	Reverse direction of isclm 24984. (Contributed by Mario Carneiro, 30-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) → 𝑊 ∈ ℂMod)
Theorem	clmzss 24998	The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂMod → ℤ ⊆ 𝐾)
Theorem	clmsscn 24999	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 25000	Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) → (𝐴 − 𝐵) = (𝐴(-g‘𝐹)𝐵))