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	oprpiece1res1 25001*	Restriction to the first part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐴 ≤ 𝐵    &   ⊢ 𝑅 ∈ V    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐾 ∈ (𝐴[,]𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝐶 ↦ if(𝑥 ≤ 𝐾, 𝑅, 𝑆))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐾), 𝑦 ∈ 𝐶 ↦ 𝑅)    ⇒   ⊢ (𝐹 ↾ ((𝐴[,]𝐾) × 𝐶)) = 𝐺
Theorem	oprpiece1res2 25002*	Restriction to the second part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐴 ≤ 𝐵    &   ⊢ 𝑅 ∈ V    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐾 ∈ (𝐴[,]𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝐶 ↦ if(𝑥 ≤ 𝐾, 𝑅, 𝑆))    &   ⊢ (𝑥 = 𝐾 → 𝑅 = 𝑃)    &   ⊢ (𝑥 = 𝐾 → 𝑆 = 𝑄)    &   ⊢ (𝑦 ∈ 𝐶 → 𝑃 = 𝑄)    &   ⊢ 𝐺 = (𝑥 ∈ (𝐾[,]𝐵), 𝑦 ∈ 𝐶 ↦ 𝑆)    ⇒   ⊢ (𝐹 ↾ ((𝐾[,]𝐵) × 𝐶)) = 𝐺
Theorem	cnrehmeo 25003*	The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 13050 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if (ℝ × ℝ) is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.) Avoid ax-mulf 11264. (Revised by GG, 16-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnrehmeoOLD 25004*	Obsolete version of cnrehmeo 25003 as of 9-Apr-2025. (Contributed by Mario Carneiro, 25-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnheiborlem 25005*	Lemma for cnheibor 25006. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑋)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))    ⇒   ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp)
Theorem	cnheibor 25006*	Heine-Borel theorem for complex numbers. A subset of ℂ is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑋)    ⇒   ⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)))
Theorem	cnllycmp 25007	The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ 𝑛-Locally Comp
Theorem	rellycmp 25008	The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ 𝑛-Locally Comp
Theorem	bndth 25009*	The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -𝐹.) (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)
Theorem	evth 25010*	The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥))
Theorem	evth2 25011*	The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦))
Theorem	lebnumlem1 25012*	Lemma for lebnum 25015. The function 𝐹 measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ+)
Theorem	lebnumlem2 25013*	Lemma for lebnum 25015. As a finite sum of point-to-set distance functions, which are continuous by metdscn 24897, the function 𝐹 is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	lebnumlem3 25014*	Lemma for lebnum 25015. By the previous lemmas, 𝐹 is continuous and positive on a compact set, so it has a positive minimum 𝑟. Then setting 𝑑 = 𝑟 / ♯(𝑈), since for each 𝑢 ∈ 𝑈 we have ball(𝑥, 𝑑) ⊆ 𝑢 iff 𝑑 ≤ 𝑑(𝑥, 𝑋 ∖ 𝑢), if ¬ ball(𝑥, 𝑑) ⊆ 𝑢 for all 𝑢 then summing over 𝑢 yields Σ𝑢 ∈ 𝑈𝑑(𝑥, 𝑋 ∖ 𝑢) = 𝐹(𝑥) < Σ𝑢 ∈ 𝑈𝑑 = 𝑟, in contradiction to the assumption that 𝑟 is the minimum of 𝐹. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) (Revised by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	lebnum 25015*	The Lebesgue number lemma, or Lebesgue covering lemma. If 𝑋 is a compact metric space and 𝑈 is an open cover of 𝑋, then there exists a positive real number 𝑑 such that every ball of size 𝑑 (and every subset of a ball of size 𝑑, including every subset of diameter less than 𝑑) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	xlebnum 25016*	Generalize lebnum 25015 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	lebnumii 25017*	Specialize the Lebesgue number lemma lebnum 25015 to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ ((𝑈 ⊆ II ∧ (0[,]1) = ∪ 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ 𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢)
12.4.12  Path homotopy
Syntax	chtpy 25018	Extend class notation with the class of homotopies between two continuous functions.
class Htpy
Syntax	cphtpy 25019	Extend class notation with the class of path homotopies between two continuous functions.
class PHtpy
Syntax	cphtpc 25020	Extend class notation with the path homotopy relation.
class ≃ph
Definition	df-htpy 25021*	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 25022*	Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 25021) 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 25023*	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 25024	A homotopy is a continuous function. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾))
Theorem	htpyi 25025	A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻0) = (𝐹‘𝐴) ∧ (𝐴𝐻1) = (𝐺‘𝐴)))
Theorem	ishtpyd 25026*	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 25027*	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 25028*	A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐹(𝐽 Htpy 𝐾)𝐹))
Theorem	htpyco1 25029*	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ ((𝑃‘𝑥)𝐻𝑦))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐾 Htpy 𝐿)𝐺))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ((𝐹 ∘ 𝑃)(𝐽 Htpy 𝐿)(𝐺 ∘ 𝑃)))
Theorem	htpyco2 25030	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(𝐽 Htpy 𝐿)(𝑃 ∘ 𝐺)))
Theorem	htpycc 25031*	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 25032*	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 25033	A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺))
Theorem	phtpycn 25034	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 25035	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 25036	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 25037*	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 25038*	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 25039*	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 25040*	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 25041	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺)))
Theorem	phtpycc 25042*	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 25043*	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 25044	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 25045	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 25046	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 25047	Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝐹( ≃ph‘𝐽)𝐺 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1)))
Theorem	reparphti 25048*	Lemma for reparpht 25050. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) Avoid ax-mulf 11264. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn II))    &   ⊢ (𝜑 → (𝐺‘0) = 0)    &   ⊢ (𝜑 → (𝐺‘1) = 1)    &   ⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥))))    ⇒   ⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹))
Theorem	reparphtiOLD 25049*	Obsolete version of reparphti 25048 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 25050	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 25051	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 25052	Extend class notation with the concatenation operation for paths in a topological space.
class *𝑝
Syntax	comi 25053	Extend class notation with the loop space.
class Ω1
Syntax	comn 25054	Extend class notation with the higher loop spaces.
class Ω𝑛
Syntax	cpi1 25055	Extend class notation with the fundamental group.
class π1
Syntax	cpin 25056	Extend class notation with the higher homotopy groups.
class πn
Definition	df-pco 25057*	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 25058*	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 25059*	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 25060*	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 25061*	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 25062*	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 25063*	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 25064	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 25065	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 25066	The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0))
Theorem	pco1 25067	The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1))
Theorem	pcoval2 25068	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 25069	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 25070	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 25071*	Lemma for pcohtpy 25072. (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 25072	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 25073	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 25074	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 25075	Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑃 = ((0[,]1) × {𝑌})    ⇒   ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = 𝑌) → (𝐹(*𝑝‘𝐽)𝑃)( ≃ph‘𝐽)𝐹)
Theorem	pcoass 25076*	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 25077*	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 25078*	Lemma for pcorev 25079. 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 25079*	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 25080*	Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))    &   ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)})    ⇒   ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃)
Theorem	pcophtb 25081*	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 25082*	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 25083*	The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)})
Theorem	om1elbas 25084	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 25085	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 25086	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 25087	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐽 ↑ko II) = (TopSet‘𝑂))
Theorem	om1opn 25088	The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝐾 = (TopOpen‘𝑂)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → 𝐾 = ((𝐽 ↑ko II) ↾t 𝐵))
Theorem	pi1val 25089	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 25090	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 25091	Lemma for pi1buni 25092. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ 𝑂 = (𝐽 Ω1 𝑌)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝑂))    ⇒   ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽)))
Theorem	pi1buni 25092	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 25093	The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽)))
Theorem	pi1eluni 25094	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 25095	The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ 𝐺 = (𝐽 π1 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))    ⇒   ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅))
Theorem	pi1cpbl 25096	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 25097*	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 25098	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 25099	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 25100	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‘𝐽))