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 
|- ( ph -> J e. SConn )
sconnpht2.2 
|- ( ph -> F e. ( II Cn J ) )
sconnpht2.3 
|- ( ph -> G e. ( II Cn J ) )
sconnpht2.4 
|- ( ph -> ( F ` 0 ) = ( G ` 0 ) )
sconnpht2.5 
|- ( ph -> ( F ` 1 ) = ( G ` 1 ) )
Assertion sconnpht2 
|- ( ph -> F ( ~=ph ` J ) G )

Proof

Step Hyp Ref Expression
1 sconnpht2.1 
 |-  ( ph -> J e. SConn )
2 sconnpht2.2 
 |-  ( ph -> F e. ( II Cn J ) )
3 sconnpht2.3 
 |-  ( ph -> G e. ( II Cn J ) )
4 sconnpht2.4 
 |-  ( ph -> ( F ` 0 ) = ( G ` 0 ) )
5 sconnpht2.5 
 |-  ( ph -> ( F ` 1 ) = ( G ` 1 ) )
6 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) = ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) )
7 6 pcorevcl 
 |-  ( G e. ( II Cn J ) -> ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) e. ( II Cn J ) /\ ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 0 ) = ( G ` 1 ) /\ ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 1 ) = ( G ` 0 ) ) )
8 3 7 syl 
 |-  ( ph -> ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) e. ( II Cn J ) /\ ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 0 ) = ( G ` 1 ) /\ ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 1 ) = ( G ` 0 ) ) )
9 8 simp1d 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) e. ( II Cn J ) )
10 8 simp2d 
 |-  ( ph -> ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 0 ) = ( G ` 1 ) )
11 5 10 eqtr4d 
 |-  ( ph -> ( F ` 1 ) = ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 0 ) )
12 2 9 11 pcocn 
 |-  ( ph -> ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) e. ( II Cn J ) )
13 2 9 pco0 
 |-  ( ph -> ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 0 ) = ( F ` 0 ) )
14 2 9 pco1 
 |-  ( ph -> ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 1 ) = ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 1 ) )
15 8 simp3d 
 |-  ( ph -> ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 1 ) = ( G ` 0 ) )
16 4 15 eqtr4d 
 |-  ( ph -> ( F ` 0 ) = ( ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ` 1 ) )
17 14 16 eqtr4d 
 |-  ( ph -> ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 1 ) = ( F ` 0 ) )
18 13 17 eqtr4d 
 |-  ( ph -> ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 0 ) = ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 1 ) )
19 sconnpht 
 |-  ( ( J e. SConn /\ ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) e. ( II Cn J ) /\ ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 0 ) = ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 1 ) ) -> ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 0 ) } ) )
20 1 12 18 19 syl3anc 
 |-  ( ph -> ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 0 ) } ) )
21 13 sneqd 
 |-  ( ph -> { ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 0 ) } = { ( F ` 0 ) } )
22 21 xpeq2d 
 |-  ( ph -> ( ( 0 [,] 1 ) X. { ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ` 0 ) } ) = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
23 20 22 breqtrd 
 |-  ( ph -> ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
24 eqid 
 |-  ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )
25 6 24 2 3 4 5 pcophtb 
 |-  ( ph -> ( ( F ( *p ` J ) ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) ) ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) <-> F ( ~=ph ` J ) G ) )
26 23 25 mpbid 
 |-  ( ph -> F ( ~=ph ` J ) G )