Metamath Proof Explorer

Theorem sconnpht2

Description: Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses sconnpht2.1 ⊢φ→J∈SConn
sconnpht2.2 ⊢φ→F∈IICnJ
sconnpht2.3 ⊢φ→G∈IICnJ
sconnpht2.4 ⊢φ→F⁡0=G⁡0
sconnpht2.5 ⊢φ→F⁡1=G⁡1
Assertion sconnpht2 ⊢φ→F≃ph⁡JG

Proof

Step Hyp Ref Expression
1 sconnpht2.1 ⊢φ→J∈SConn
2 sconnpht2.2 ⊢φ→F∈IICnJ
3 sconnpht2.3 ⊢φ→G∈IICnJ
4 sconnpht2.4 ⊢φ→F⁡0=G⁡0
5 sconnpht2.5 ⊢φ→F⁡1=G⁡1
6 eqid ⊢x∈01⟼G⁡1−x=x∈01⟼G⁡1−x
7 6 pcorevcl ⊢G∈IICnJ→x∈01⟼G⁡1−x∈IICnJ∧x∈01⟼G⁡1−x⁡0=G⁡1∧x∈01⟼G⁡1−x⁡1=G⁡0
8 3 7 syl ⊢φ→x∈01⟼G⁡1−x∈IICnJ∧x∈01⟼G⁡1−x⁡0=G⁡1∧x∈01⟼G⁡1−x⁡1=G⁡0
9 8 simp1d ⊢φ→x∈01⟼G⁡1−x∈IICnJ
10 8 simp2d ⊢φ→x∈01⟼G⁡1−x⁡0=G⁡1
11 5 10 eqtr4d ⊢φ→F⁡1=x∈01⟼G⁡1−x⁡0
12 2 9 11 pcocn ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x∈IICnJ
13 2 9 pco0 ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x⁡0=F⁡0
14 2 9 pco1 ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x⁡1=x∈01⟼G⁡1−x⁡1
15 8 simp3d ⊢φ→x∈01⟼G⁡1−x⁡1=G⁡0
16 4 15 eqtr4d ⊢φ→F⁡0=x∈01⟼G⁡1−x⁡1
17 14 16 eqtr4d ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x⁡1=F⁡0
18 13 17 eqtr4d ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x⁡0=F*𝑝⁡Jx∈01⟼G⁡1−x⁡1
19 sconnpht ⊢J∈SConn∧F*𝑝⁡Jx∈01⟼G⁡1−x∈IICnJ∧F*𝑝⁡Jx∈01⟼G⁡1−x⁡0=F*𝑝⁡Jx∈01⟼G⁡1−x⁡1→F*𝑝⁡Jx∈01⟼G⁡1−x≃ph⁡J01×F*𝑝⁡Jx∈01⟼G⁡1−x⁡0
20 1 12 18 19 syl3anc ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x≃ph⁡J01×F*𝑝⁡Jx∈01⟼G⁡1−x⁡0
21 13 sneqd ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x⁡0=F⁡0
22 21 xpeq2d ⊢φ→01×F*𝑝⁡Jx∈01⟼G⁡1−x⁡0=01×F⁡0
23 20 22 breqtrd ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x≃ph⁡J01×F⁡0
24 eqid ⊢01×F⁡0=01×F⁡0
25 6 24 2 3 4 5 pcophtb ⊢φ→F*𝑝⁡Jx∈01⟼G⁡1−x≃ph⁡J01×F⁡0↔F≃ph⁡JG
26 23 25 mpbid ⊢φ→F≃ph⁡JG