Metamath Proof Explorer

Theorem phtpyco2

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

Ref Expression
Hypotheses phtpyco2.f 
|- ( ph -> F e. ( II Cn J ) )
phtpyco2.g 
|- ( ph -> G e. ( II Cn J ) )
phtpyco2.p 
|- ( ph -> P e. ( J Cn K ) )
phtpyco2.h 
|- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
Assertion phtpyco2 
|- ( ph -> ( P o. H ) e. ( ( P o. F ) ( PHtpy ` K ) ( P o. G ) ) )

Proof

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