P. 249 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24801-24900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abscncf 24801	Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ abs ∈ (ℂ–cn→ℝ)
Theorem	recncf 24802	Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℜ ∈ (ℂ–cn→ℝ)
Theorem	imcncf 24803	Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℑ ∈ (ℂ–cn→ℝ)
Theorem	cjcncf 24804	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ∗ ∈ (ℂ–cn→ℂ)
Theorem	mulc1cncf 24805*	Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	divccncf 24806*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cncfco 24807	The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶))
Theorem	cncfcompt2 24808*	Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑆) ∈ (𝐶–cn→𝐸))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑇) ∈ (𝐴–cn→𝐸))
Theorem	cncfmet 24809	Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ 𝐶 = ((abs ∘ − ) ↾ (𝐴 × 𝐴))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐽 Cn 𝐾))
Theorem	cncfcn 24810	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐴)    &   ⊢ 𝐿 = (𝐽 ↾t 𝐵)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿))
Theorem	cncfcn1 24811	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (ℂ–cn→ℂ) = (𝐽 Cn 𝐽)
Theorem	cncfmptc 24812*	A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ ((𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→𝑇))
Theorem	cncfmptid 24813*	The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝑥) ∈ (𝑆–cn→𝑇))
Theorem	cncfmpt1f 24814*	Composition of continuous functions. –cn→ analogue of cnmpt11f 23558. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmpt2f 24815*	Composition of continuous functions. –cn→ analogue of cnmpt12f 23560. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmpt2ss 24816*	Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→𝑆))    &   ⊢ 𝑆 ⊆ ℂ    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→𝑆))
Theorem	addccncf 24817*	Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	idcncf 24818	The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 24813 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝑥)    ⇒   ⊢ 𝐹 ∈ (ℂ–cn→ℂ)
Theorem	sub1cncf 24819*	Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	sub2cncf 24820*	Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cdivcncf 24821*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ((ℂ ∖ {0})–cn→ℂ))
Theorem	negcncf 24822*	The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) Avoid ax-mulf 11155. (Revised by GG, 16-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥)    ⇒   ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	negcncfOLD 24823*	Obsolete version of negcncf 24822 as of 9-Apr-2025. (Contributed by Mario Carneiro, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥)    ⇒   ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	negfcncf 24824*	The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝑥))    ⇒   ⊢ (𝐹 ∈ (𝐴–cn→ℂ) → 𝐺 ∈ (𝐴–cn→ℂ))
Theorem	abscncfALT 24825	Absolute value is continuous. Alternate proof of abscncf 24801. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ abs ∈ (ℂ–cn→ℝ)
Theorem	cncfcnvcn 24826	Rewrite cmphaushmeo 23694 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑋)    ⇒   ⊢ ((𝐾 ∈ Comp ∧ 𝐹 ∈ (𝑋–cn→𝑌)) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑌–cn→𝑋)))
Theorem	expcncf 24827*	The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 24770. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ))
Theorem	cnmptre 24828*	Lemma for iirevcn 24831 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ 𝑅 = (TopOpen‘ℂfld)    &   ⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    &   ⊢ 𝐾 = ((topGen‘ran (,)) ↾t 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐹) ∈ (𝑅 Cn 𝑅))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐽 Cn 𝐾))
Theorem	cnmpopc 24829*	Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ 𝑅 = (topGen‘ran (,))    &   ⊢ 𝑀 = (𝑅 ↾t (𝐴[,]𝐵))    &   ⊢ 𝑁 = (𝑅 ↾t (𝐵[,]𝐶))    &   ⊢ 𝑂 = (𝑅 ↾t (𝐴[,]𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐵 ∧ 𝑦 ∈ 𝑋)) → 𝐷 = 𝐸)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ 𝐷) ∈ ((𝑀 ×t 𝐽) Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ 𝐸) ∈ ((𝑁 ×t 𝐽) Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑂 ×t 𝐽) Cn 𝐾))
Theorem	iirev 24830	Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ (0[,]1) → (1 − 𝑋) ∈ (0[,]1))
Theorem	iirevcn 24831	The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn II)
Theorem	iihalf1 24832	Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ (0[,](1 / 2)) → (2 · 𝑋) ∈ (0[,]1))
Theorem	iihalf1cn 24833	The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11155. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))    ⇒   ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II)
Theorem	iihalf1cnOLD 24834	Obsolete version of iihalf1cn 24833 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))    ⇒   ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II)
Theorem	iihalf2 24835	Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ ((1 / 2)[,]1) → ((2 · 𝑋) − 1) ∈ (0[,]1))
Theorem	iihalf2cn 24836	The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11155. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))    ⇒   ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II)
Theorem	iihalf2cnOLD 24837	Obsolete version of iihalf2cn 24836 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))    ⇒   ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II)
Theorem	elii1 24838	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
⊢ (𝑋 ∈ (0[,](1 / 2)) ↔ (𝑋 ∈ (0[,]1) ∧ 𝑋 ≤ (1 / 2)))
Theorem	elii2 24839	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬ 𝑋 ≤ (1 / 2)) → 𝑋 ∈ ((1 / 2)[,]1))
Theorem	iimulcl 24840	The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1)) → (𝐴 · 𝐵) ∈ (0[,]1))
Theorem	iimulcn 24841*	Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.) Avoid ax-mulf 11155. (Revised by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II)
Theorem	iimulcnOLD 24842*	Obsolete version of iimulcn 24841 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II)
Theorem	icoopnst 24843	A half-open interval starting at 𝐴 is open in the closed interval from 𝐴 to 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) → (𝐴[,)𝐶) ∈ 𝐽))
Theorem	iocopnst 24844	A half-open interval ending at 𝐵 is open in the closed interval from 𝐴 to 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,)𝐵) → (𝐶(,]𝐵) ∈ 𝐽))
Theorem	icchmeo 24845*	The natural bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) Avoid ax-mulf 11155. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))))
Theorem	icchmeoOLD 24846*	Obsolete version of icchmeo 24845 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))))
Theorem	icopnfcnv 24847*	Define a bijection from [0, 1) to [0, +∞). (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))    ⇒   ⊢ (𝐹:(0[,)1)–1-1-onto→(0[,)+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,)+∞) ↦ (𝑦 / (1 + 𝑦))))
Theorem	icopnfhmeo 24848*	The defined bijection from [0, 1) to [0, +∞) is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐹 Isom < , < ((0[,)1), (0[,)+∞)) ∧ 𝐹 ∈ ((𝐽 ↾t (0[,)1))Homeo(𝐽 ↾t (0[,)+∞))))
Theorem	iccpnfcnv 24849*	Define a bijection from [0, 1] to [0, +∞]. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))    ⇒   ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦)))))
Theorem	iccpnfhmeo 24850	The defined bijection from [0, 1] to [0, +∞] is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))    &   ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo𝐾))
Theorem	xrhmeo 24851*	The bijection from [-1, 1] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))    &   ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -𝑒(𝐹‘-𝑦)))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 ↾t (-1[,]1))Homeo(ordTop‘ ≤ )))
Theorem	xrhmph 24852	The extended reals are homeomorphic to the interval [0, 1]. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ II ≃ (ordTop‘ ≤ )
Theorem	xrcmp 24853	The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 24702), this means that ℝ* is a compactification of ℝ. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Comp
Theorem	xrconn 24854	The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Conn
Theorem	icccvx 24855	A linear combination of two reals lies in the interval between them. Equivalently, a closed interval is a convex set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐷 ∈ (𝐴[,]𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐶) + (𝑇 · 𝐷)) ∈ (𝐴[,]𝐵)))
Theorem	oprpiece1res1 24856*	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 24857*	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 24858*	The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 12951 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 11155. (Revised by GG, 16-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnrehmeoOLD 24859*	Obsolete version of cnrehmeo 24858 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 24860*	Lemma for cnheibor 24861. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑋)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))    ⇒   ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp)
Theorem	cnheibor 24861*	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 24862	The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ 𝑛-Locally Comp
Theorem	rellycmp 24863	The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ 𝑛-Locally Comp
Theorem	bndth 24864*	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 24865*	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 24866*	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 24867*	Lemma for lebnum 24870. 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 24868*	Lemma for lebnum 24870. As a finite sum of point-to-set distance functions, which are continuous by metdscn 24752, 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 24869*	Lemma for lebnum 24870. 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 24870*	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 24871*	Generalize lebnum 24870 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	lebnumii 24872*	Specialize the Lebesgue number lemma lebnum 24870 to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ ((𝑈 ⊆ II ∧ (0[,]1) = ∪ 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ 𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢)
12.4.12  Path homotopy
Syntax	chtpy 24873	Extend class notation with the class of homotopies between two continuous functions.
class Htpy
Syntax	cphtpy 24874	Extend class notation with the class of path homotopies between two continuous functions.
class PHtpy
Syntax	cphtpc 24875	Extend class notation with the path homotopy relation.
class ≃ph
Definition	df-htpy 24876*	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 24877*	Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 24876) 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 24878*	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 24879	A homotopy is a continuous function. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾))
Theorem	htpyi 24880	A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻0) = (𝐹‘𝐴) ∧ (𝐴𝐻1) = (𝐺‘𝐴)))
Theorem	ishtpyd 24881*	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 24882*	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 24883*	A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐹(𝐽 Htpy 𝐾)𝐹))
Theorem	htpyco1 24884*	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ ((𝑃‘𝑥)𝐻𝑦))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐾 Htpy 𝐿)𝐺))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ((𝐹 ∘ 𝑃)(𝐽 Htpy 𝐿)(𝐺 ∘ 𝑃)))
Theorem	htpyco2 24885	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐾 Cn 𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(𝐽 Htpy 𝐿)(𝑃 ∘ 𝐺)))
Theorem	htpycc 24886*	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 24887*	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 24888	A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺))
Theorem	phtpycn 24889	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 24890	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 24891	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 24892*	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 24893*	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 24894*	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 24895*	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 24896	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))    ⇒   ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺)))
Theorem	phtpycc 24897*	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 24898*	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 24899	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 24900	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‘𝐽)𝐺) ≠ ∅))