Metamath Proof Explorer

Theorem htpyco2

Description: Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses htpyco2.f 
|- ( ph -> F e. ( J Cn K ) )
htpyco2.g 
|- ( ph -> G e. ( J Cn K ) )
htpyco2.p 
|- ( ph -> P e. ( K Cn L ) )
htpyco2.h 
|- ( ph -> H e. ( F ( J Htpy K ) G ) )
Assertion htpyco2 
|- ( ph -> ( P o. H ) e. ( ( P o. F ) ( J Htpy L ) ( P o. G ) ) )

Proof

Step Hyp Ref Expression
1 htpyco2.f 
 |-  ( ph -> F e. ( J Cn K ) )
2 htpyco2.g 
 |-  ( ph -> G e. ( J Cn K ) )
3 htpyco2.p 
 |-  ( ph -> P e. ( K Cn L ) )
4 htpyco2.h 
 |-  ( ph -> H e. ( F ( J Htpy K ) G ) )
5 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
6 1 5 syl 
 |-  ( ph -> J e. Top )
7 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
8 6 7 sylib 
 |-  ( ph -> J e. ( TopOn ` U. J ) )
9 cnco 
 |-  ( ( F e. ( J Cn K ) /\ P e. ( K Cn L ) ) -> ( P o. F ) e. ( J Cn L ) )
10 1 3 9 syl2anc 
 |-  ( ph -> ( P o. F ) e. ( J Cn L ) )
11 cnco 
 |-  ( ( G e. ( J Cn K ) /\ P e. ( K Cn L ) ) -> ( P o. G ) e. ( J Cn L ) )
12 2 3 11 syl2anc 
 |-  ( ph -> ( P o. G ) e. ( J Cn L ) )
13 8 1 2 htpycn 
 |-  ( ph -> ( F ( J Htpy K ) G ) C_ ( ( J tX II ) Cn K ) )
14 13 4 sseldd 
 |-  ( ph -> H e. ( ( J tX II ) Cn K ) )
15 cnco 
 |-  ( ( H e. ( ( J tX II ) Cn K ) /\ P e. ( K Cn L ) ) -> ( P o. H ) e. ( ( J tX II ) Cn L ) )
16 14 3 15 syl2anc 
 |-  ( ph -> ( P o. H ) e. ( ( J tX II ) Cn L ) )
17 8 1 2 4 htpyi 
 |-  ( ( ph /\ s e. U. J ) -> ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) )
18 17 simpld 
 |-  ( ( ph /\ s e. U. J ) -> ( s H 0 ) = ( F ` s ) )
19 18 fveq2d 
 |-  ( ( ph /\ s e. U. J ) -> ( P ` ( s H 0 ) ) = ( P ` ( F ` s ) ) )
20 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
21 txtopon 
 |-  ( ( J e. ( TopOn ` U. J ) /\ II e. ( TopOn ` ( 0 [,] 1 ) ) ) -> ( J tX II ) e. ( TopOn ` ( U. J X. ( 0 [,] 1 ) ) ) )
22 8 20 21 sylancl 
 |-  ( ph -> ( J tX II ) e. ( TopOn ` ( U. J X. ( 0 [,] 1 ) ) ) )
23 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
24 1 23 syl 
 |-  ( ph -> K e. Top )
25 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
26 24 25 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
27 cnf2 
 |-  ( ( ( J tX II ) e. ( TopOn ` ( U. J X. ( 0 [,] 1 ) ) ) /\ K e. ( TopOn ` U. K ) /\ H e. ( ( J tX II ) Cn K ) ) -> H : ( U. J X. ( 0 [,] 1 ) ) --> U. K )
28 22 26 14 27 syl3anc 
 |-  ( ph -> H : ( U. J X. ( 0 [,] 1 ) ) --> U. K )
29 simpr 
 |-  ( ( ph /\ s e. U. J ) -> s e. U. J )
30 0elunit 
 |-  0 e. ( 0 [,] 1 )
31 opelxpi 
 |-  ( ( s e. U. J /\ 0 e. ( 0 [,] 1 ) ) -> <. s , 0 >. e. ( U. J X. ( 0 [,] 1 ) ) )
32 29 30 31 sylancl 
 |-  ( ( ph /\ s e. U. J ) -> <. s , 0 >. e. ( U. J X. ( 0 [,] 1 ) ) )
33 fvco3 
 |-  ( ( H : ( U. J X. ( 0 [,] 1 ) ) --> U. K /\ <. s , 0 >. e. ( U. J X. ( 0 [,] 1 ) ) ) -> ( ( P o. H ) ` <. s , 0 >. ) = ( P ` ( H ` <. s , 0 >. ) ) )
34 28 32 33 syl2an2r 
 |-  ( ( ph /\ s e. U. J ) -> ( ( P o. H ) ` <. s , 0 >. ) = ( P ` ( H ` <. s , 0 >. ) ) )
35 df-ov 
 |-  ( s ( P o. H ) 0 ) = ( ( P o. H ) ` <. s , 0 >. )
36 df-ov 
 |-  ( s H 0 ) = ( H ` <. s , 0 >. )
37 36 fveq2i 
 |-  ( P ` ( s H 0 ) ) = ( P ` ( H ` <. s , 0 >. ) )
38 34 35 37 3eqtr4g 
 |-  ( ( ph /\ s e. U. J ) -> ( s ( P o. H ) 0 ) = ( P ` ( s H 0 ) ) )
39 eqid 
 |-  U. J = U. J
40 eqid 
 |-  U. K = U. K
41 39 40 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
42 1 41 syl 
 |-  ( ph -> F : U. J --> U. K )
43 fvco3 
 |-  ( ( F : U. J --> U. K /\ s e. U. J ) -> ( ( P o. F ) ` s ) = ( P ` ( F ` s ) ) )
44 42 43 sylan 
 |-  ( ( ph /\ s e. U. J ) -> ( ( P o. F ) ` s ) = ( P ` ( F ` s ) ) )
45 19 38 44 3eqtr4d 
 |-  ( ( ph /\ s e. U. J ) -> ( s ( P o. H ) 0 ) = ( ( P o. F ) ` s ) )
46 17 simprd 
 |-  ( ( ph /\ s e. U. J ) -> ( s H 1 ) = ( G ` s ) )
47 46 fveq2d 
 |-  ( ( ph /\ s e. U. J ) -> ( P ` ( s H 1 ) ) = ( P ` ( G ` s ) ) )
48 1elunit 
 |-  1 e. ( 0 [,] 1 )
49 opelxpi 
 |-  ( ( s e. U. J /\ 1 e. ( 0 [,] 1 ) ) -> <. s , 1 >. e. ( U. J X. ( 0 [,] 1 ) ) )
50 29 48 49 sylancl 
 |-  ( ( ph /\ s e. U. J ) -> <. s , 1 >. e. ( U. J X. ( 0 [,] 1 ) ) )
51 fvco3 
 |-  ( ( H : ( U. J X. ( 0 [,] 1 ) ) --> U. K /\ <. s , 1 >. e. ( U. J X. ( 0 [,] 1 ) ) ) -> ( ( P o. H ) ` <. s , 1 >. ) = ( P ` ( H ` <. s , 1 >. ) ) )
52 28 50 51 syl2an2r 
 |-  ( ( ph /\ s e. U. J ) -> ( ( P o. H ) ` <. s , 1 >. ) = ( P ` ( H ` <. s , 1 >. ) ) )
53 df-ov 
 |-  ( s ( P o. H ) 1 ) = ( ( P o. H ) ` <. s , 1 >. )
54 df-ov 
 |-  ( s H 1 ) = ( H ` <. s , 1 >. )
55 54 fveq2i 
 |-  ( P ` ( s H 1 ) ) = ( P ` ( H ` <. s , 1 >. ) )
56 52 53 55 3eqtr4g 
 |-  ( ( ph /\ s e. U. J ) -> ( s ( P o. H ) 1 ) = ( P ` ( s H 1 ) ) )
57 39 40 cnf 
 |-  ( G e. ( J Cn K ) -> G : U. J --> U. K )
58 2 57 syl 
 |-  ( ph -> G : U. J --> U. K )
59 fvco3 
 |-  ( ( G : U. J --> U. K /\ s e. U. J ) -> ( ( P o. G ) ` s ) = ( P ` ( G ` s ) ) )
60 58 59 sylan 
 |-  ( ( ph /\ s e. U. J ) -> ( ( P o. G ) ` s ) = ( P ` ( G ` s ) ) )
61 47 56 60 3eqtr4d 
 |-  ( ( ph /\ s e. U. J ) -> ( s ( P o. H ) 1 ) = ( ( P o. G ) ` s ) )
62 8 10 12 16 45 61 ishtpyd 
 |-  ( ph -> ( P o. H ) e. ( ( P o. F ) ( J Htpy L ) ( P o. G ) ) )