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 φJSConn
sconnpht2.2 φFIICnJ
sconnpht2.3 φGIICnJ
sconnpht2.4 φF0=G0
sconnpht2.5 φF1=G1
Assertion sconnpht2 φFphJG

Proof

Step Hyp Ref Expression
1 sconnpht2.1 φJSConn
2 sconnpht2.2 φFIICnJ
3 sconnpht2.3 φGIICnJ
4 sconnpht2.4 φF0=G0
5 sconnpht2.5 φF1=G1
6 eqid x01G1x=x01G1x
7 6 pcorevcl GIICnJx01G1xIICnJx01G1x0=G1x01G1x1=G0
8 3 7 syl φx01G1xIICnJx01G1x0=G1x01G1x1=G0
9 8 simp1d φx01G1xIICnJ
10 8 simp2d φx01G1x0=G1
11 5 10 eqtr4d φF1=x01G1x0
12 2 9 11 pcocn φF*𝑝Jx01G1xIICnJ
13 2 9 pco0 φF*𝑝Jx01G1x0=F0
14 2 9 pco1 φF*𝑝Jx01G1x1=x01G1x1
15 8 simp3d φx01G1x1=G0
16 4 15 eqtr4d φF0=x01G1x1
17 14 16 eqtr4d φF*𝑝Jx01G1x1=F0
18 13 17 eqtr4d φF*𝑝Jx01G1x0=F*𝑝Jx01G1x1
19 sconnpht JSConnF*𝑝Jx01G1xIICnJF*𝑝Jx01G1x0=F*𝑝Jx01G1x1F*𝑝Jx01G1xphJ01×F*𝑝Jx01G1x0
20 1 12 18 19 syl3anc φF*𝑝Jx01G1xphJ01×F*𝑝Jx01G1x0
21 13 sneqd φF*𝑝Jx01G1x0=F0
22 21 xpeq2d φ01×F*𝑝Jx01G1x0=01×F0
23 20 22 breqtrd φF*𝑝Jx01G1xphJ01×F0
24 eqid 01×F0=01×F0
25 6 24 2 3 4 5 pcophtb φF*𝑝Jx01G1xphJ01×F0FphJG
26 23 25 mpbid φFphJG