Metamath Proof Explorer

Theorem pcohtpy

Description: Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses pcohtpy.4 
|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
pcohtpy.5 
|- ( ph -> F ( ~=ph ` J ) H )
pcohtpy.6 
|- ( ph -> G ( ~=ph ` J ) K )
Assertion pcohtpy 
|- ( ph -> ( F ( *p ` J ) G ) ( ~=ph ` J ) ( H ( *p ` J ) K ) )

Proof

Step Hyp Ref Expression
1 pcohtpy.4 
 |-  ( ph -> ( F ` 1 ) = ( G ` 0 ) )
2 pcohtpy.5 
 |-  ( ph -> F ( ~=ph ` J ) H )
3 pcohtpy.6 
 |-  ( ph -> G ( ~=ph ` J ) K )
4 isphtpc 
 |-  ( F ( ~=ph ` J ) H <-> ( F e. ( II Cn J ) /\ H e. ( II Cn J ) /\ ( F ( PHtpy ` J ) H ) =/= (/) ) )
5 2 4 sylib 
 |-  ( ph -> ( F e. ( II Cn J ) /\ H e. ( II Cn J ) /\ ( F ( PHtpy ` J ) H ) =/= (/) ) )
6 5 simp1d 
 |-  ( ph -> F e. ( II Cn J ) )
7 isphtpc 
 |-  ( G ( ~=ph ` J ) K <-> ( G e. ( II Cn J ) /\ K e. ( II Cn J ) /\ ( G ( PHtpy ` J ) K ) =/= (/) ) )
8 3 7 sylib 
 |-  ( ph -> ( G e. ( II Cn J ) /\ K e. ( II Cn J ) /\ ( G ( PHtpy ` J ) K ) =/= (/) ) )
9 8 simp1d 
 |-  ( ph -> G e. ( II Cn J ) )
10 6 9 1 pcocn 
 |-  ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )
11 5 simp2d 
 |-  ( ph -> H e. ( II Cn J ) )
12 8 simp2d 
 |-  ( ph -> K e. ( II Cn J ) )
13 phtpc01 
 |-  ( F ( ~=ph ` J ) H -> ( ( F ` 0 ) = ( H ` 0 ) /\ ( F ` 1 ) = ( H ` 1 ) ) )
14 2 13 syl 
 |-  ( ph -> ( ( F ` 0 ) = ( H ` 0 ) /\ ( F ` 1 ) = ( H ` 1 ) ) )
15 14 simprd 
 |-  ( ph -> ( F ` 1 ) = ( H ` 1 ) )
16 phtpc01 
 |-  ( G ( ~=ph ` J ) K -> ( ( G ` 0 ) = ( K ` 0 ) /\ ( G ` 1 ) = ( K ` 1 ) ) )
17 3 16 syl 
 |-  ( ph -> ( ( G ` 0 ) = ( K ` 0 ) /\ ( G ` 1 ) = ( K ` 1 ) ) )
18 17 simpld 
 |-  ( ph -> ( G ` 0 ) = ( K ` 0 ) )
19 1 15 18 3eqtr3d 
 |-  ( ph -> ( H ` 1 ) = ( K ` 0 ) )
20 11 12 19 pcocn 
 |-  ( ph -> ( H ( *p ` J ) K ) e. ( II Cn J ) )
21 5 simp3d 
 |-  ( ph -> ( F ( PHtpy ` J ) H ) =/= (/) )
22 n0 
 |-  ( ( F ( PHtpy ` J ) H ) =/= (/) <-> E. m m e. ( F ( PHtpy ` J ) H ) )
23 21 22 sylib 
 |-  ( ph -> E. m m e. ( F ( PHtpy ` J ) H ) )
24 8 simp3d 
 |-  ( ph -> ( G ( PHtpy ` J ) K ) =/= (/) )
25 n0 
 |-  ( ( G ( PHtpy ` J ) K ) =/= (/) <-> E. n n e. ( G ( PHtpy ` J ) K ) )
26 24 25 sylib 
 |-  ( ph -> E. n n e. ( G ( PHtpy ` J ) K ) )
27 exdistrv 
 |-  ( E. m E. n ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) <-> ( E. m m e. ( F ( PHtpy ` J ) H ) /\ E. n n e. ( G ( PHtpy ` J ) K ) ) )
28 23 26 27 sylanbrc 
 |-  ( ph -> E. m E. n ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) )
29 1 adantr 
 |-  ( ( ph /\ ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) ) -> ( F ` 1 ) = ( G ` 0 ) )
30 2 adantr 
 |-  ( ( ph /\ ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) ) -> F ( ~=ph ` J ) H )
31 3 adantr 
 |-  ( ( ph /\ ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) ) -> G ( ~=ph ` J ) K )
32 eqid 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) m y ) , ( ( ( 2 x. x ) - 1 ) n y ) ) ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) m y ) , ( ( ( 2 x. x ) - 1 ) n y ) ) )
33 simprl 
 |-  ( ( ph /\ ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) ) -> m e. ( F ( PHtpy ` J ) H ) )
34 simprr 
 |-  ( ( ph /\ ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) ) -> n e. ( G ( PHtpy ` J ) K ) )
35 29 30 31 32 33 34 pcohtpylem 
 |-  ( ( ph /\ ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) ) -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) m y ) , ( ( ( 2 x. x ) - 1 ) n y ) ) ) e. ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) )
36 35 ne0d 
 |-  ( ( ph /\ ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) ) -> ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) =/= (/) )
37 36 ex 
 |-  ( ph -> ( ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) -> ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) =/= (/) ) )
38 37 exlimdvv 
 |-  ( ph -> ( E. m E. n ( m e. ( F ( PHtpy ` J ) H ) /\ n e. ( G ( PHtpy ` J ) K ) ) -> ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) =/= (/) ) )
39 28 38 mpd 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) =/= (/) )
40 isphtpc 
 |-  ( ( F ( *p ` J ) G ) ( ~=ph ` J ) ( H ( *p ` J ) K ) <-> ( ( F ( *p ` J ) G ) e. ( II Cn J ) /\ ( H ( *p ` J ) K ) e. ( II Cn J ) /\ ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) =/= (/) ) )
41 10 20 39 40 syl3anbrc 
 |-  ( ph -> ( F ( *p ` J ) G ) ( ~=ph ` J ) ( H ( *p ` J ) K ) )