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	xlebnum 24901*	Generalize lebnum 24900 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	lebnumii 24902*	Specialize the Lebesgue number lemma lebnum 24900 to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ ((𝑈 ⊆ II ∧ (0[,]1) = ∪ 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ 𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢)
12.4.12  Path homotopy
Syntax	chtpy 24903	Extend class notation with the class of homotopies between two continuous functions.
class Htpy
Syntax	cphtpy 24904	Extend class notation with the class of path homotopies between two continuous functions.
class PHtpy
Syntax	cphtpc 24905	Extend class notation with the path homotopy relation.
class ≃ph
Definition	df-htpy 24906*	Define the function which takes topological spaces 𝑋, 𝑌 and two continuous functions 𝐹, 𝐺:𝑋⟶𝑌 and returns the class of homotopies from 𝐹 to 𝐺. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ Htpy = (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ {ℎ ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}))
Definition	df-phtpy 24907*	Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 24906) which also preserve both endpoints of the paths throughout the homotopy. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ PHtpy = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))
Theorem	ishtpy 24908*	Membership in the class of homotopies between two continuous functions. (Contributed by Mario Carneiro, 22-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺) ↔ (𝐻 ∈ ((𝐽 ×t II) Cn 𝐾) ∧ ∀𝑠 ∈ 𝑋 ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠)))))
Theorem	htpycn 24909	A homotopy is a continuous function. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾))
Theorem	htpyi 24910	A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻0) = (𝐹‘𝐴) ∧ (𝐴𝐻1) = (𝐺‘𝐴)))
Theorem	ishtpyd 24911*	Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ ((𝐽 ×t II) Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐻0) = (𝐹‘𝑠))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐻1) = (𝐺‘𝑠))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))
Theorem	htpycom 24912*	Given a homotopy from 𝐹 to 𝐺, produce a homotopy from 𝐺 to 𝐹. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ 𝑀 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ (𝑥𝐻(1 − 𝑦)))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝐺(𝐽 Htpy 𝐾)𝐹))
Theorem	htpyid 24913*	A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐹(𝐽 Htpy 𝐾)𝐹))
Theorem	htpyco1 24914*	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ ((𝑃‘𝑥)𝐻𝑦))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐾 Htpy 𝐿)𝐺))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ((𝐹 ∘ 𝑃)(𝐽 Htpy 𝐿)(𝐺 ∘ 𝑃)))
Theorem	htpyco2 24915	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(𝐽 Htpy 𝐿)(𝑃 ∘ 𝐺)))
Theorem	htpycc 24916*	Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1))))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    &   ⊢ (𝜑 → 𝑀 ∈ (𝐺(𝐽 Htpy 𝐾)𝐻))    ⇒   ⊢ (𝜑 → 𝑁 ∈ (𝐹(𝐽 Htpy 𝐾)𝐻))
Theorem	isphtpy 24917*	Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺) ↔ (𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺) ∧ ∀𝑠 ∈ (0[,]1)((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1)))))
Theorem	phtpyhtpy 24918	A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺))
Theorem	phtpycn 24919	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 24920	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 24921	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 24922*	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 24923*	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 24924*	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 24925*	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 24926	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺)))
Theorem	phtpycc 24927*	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 24928*	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 24929	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 24930	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 24931	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 24932	Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝐹( ≃ph‘𝐽)𝐺 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1)))
Theorem	reparphti 24933*	Lemma for reparpht 24935. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) Avoid ax-mulf 11096. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn II))    &   ⊢ (𝜑 → (𝐺‘0) = 0)    &   ⊢ (𝜑 → (𝐺‘1) = 1)    &   ⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))))    ⇒   ⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹))
Theorem	reparphtiOLD 24934*	Obsolete version of reparphti 24933 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 24935	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 24936	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 24937	Extend class notation with the concatenation operation for paths in a topological space.
class *𝑝
Syntax	comi 24938	Extend class notation with the loop space.
class Ω1
Syntax	comn 24939	Extend class notation with the higher loop spaces.
class Ω𝑛
Syntax	cpi1 24940	Extend class notation with the fundamental group.
class π1
Syntax	cpin 24941	Extend class notation with the higher homotopy groups.
class πn
Definition	df-pco 24942*	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 24943*	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 24944*	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 24945*	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 24946*	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 24947*	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 24948*	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 24949	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 24950	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 24951	The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0))
Theorem	pco1 24952	The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1))
Theorem	pcoval2 24953	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 24954	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 24955	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 24956*	Lemma for pcohtpy 24957. (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 24957	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 24958	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 24959	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 24960	Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑃 = ((0[,]1) × {𝑌})    ⇒   ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = 𝑌) → (𝐹(*𝑝‘𝐽)𝑃)( ≃ph‘𝐽)𝐹)
Theorem	pcoass 24961*	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 24962*	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 24963*	Lemma for pcorev 24964. 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 24964*	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 24965*	Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)})    ⇒   ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃)
Theorem	pcophtb 24966*	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 24967*	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 24968*	The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)})
Theorem	om1elbas 24969	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 24970	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 24971	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 24972	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐽 ↑ko II) = (TopSet‘𝑂))
Theorem	om1opn 24973	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝐾 = (TopOpen‘𝑂)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐾 = ((𝐽 ↑ko II) ↾t 𝐵))
Theorem	pi1val 24974	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 24975	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 24976	Lemma for pi1buni 24977. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽)))
Theorem	pi1buni 24977	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 24978	The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽)))
Theorem	pi1eluni 24979	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 24980	The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅))
Theorem	pi1cpbl 24981	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 24982*	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 24983	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 24984	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 24985	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 24986	Lemma for pi1grp 24987. (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 24987	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 24988	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 24989*	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 24990*	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 24991*	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 24992*	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 24993*	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 24994*	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 24995*	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 24996*	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 24997*	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 24998*	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 24999	Syntax for the class of subcomplex modules.
class ℂMod
Definition	df-clm 25000*	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 20500), left modules over such subrings are the same as right modules, see rmodislmod 20873. 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))}