Metamath Proof Explorer

Theorem copco

Description: The composition of a concatenation of paths with a continuous function. (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses pcoval.2 
|- ( ph -> F e. ( II Cn J ) )
pcoval.3 
|- ( ph -> G e. ( II Cn J ) )
pcoval2.4 
|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
copco.6 
|- ( ph -> H e. ( J Cn K ) )
Assertion copco 
|- ( ph -> ( H o. ( F ( *p ` J ) G ) ) = ( ( H o. F ) ( *p ` K ) ( H o. G ) ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 pcoval.3 
 |-  ( ph -> G e. ( II Cn J ) )
3 pcoval2.4 
 |-  ( ph -> ( F ` 1 ) = ( G ` 0 ) )
4 copco.6 
 |-  ( ph -> H e. ( J Cn K ) )
5 iiuni 
 |-  ( 0 [,] 1 ) = U. II
6 eqid 
 |-  U. J = U. J
7 5 6 cnf 
 |-  ( F e. ( II Cn J ) -> F : ( 0 [,] 1 ) --> U. J )
8 1 7 syl 
 |-  ( ph -> F : ( 0 [,] 1 ) --> U. J )
9 elii1 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) <-> ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 2 ) ) )
10 iihalf1 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. x ) e. ( 0 [,] 1 ) )
11 9 10 sylbir 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 2 ) ) -> ( 2 x. x ) e. ( 0 [,] 1 ) )
12 fvco3 
 |-  ( ( F : ( 0 [,] 1 ) --> U. J /\ ( 2 x. x ) e. ( 0 [,] 1 ) ) -> ( ( H o. F ) ` ( 2 x. x ) ) = ( H ` ( F ` ( 2 x. x ) ) ) )
13 8 11 12 syl2an 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 2 ) ) ) -> ( ( H o. F ) ` ( 2 x. x ) ) = ( H ` ( F ` ( 2 x. x ) ) ) )
14 13 anassrs 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( ( H o. F ) ` ( 2 x. x ) ) = ( H ` ( F ` ( 2 x. x ) ) ) )
15 5 6 cnf 
 |-  ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> U. J )
16 2 15 syl 
 |-  ( ph -> G : ( 0 [,] 1 ) --> U. J )
17 elii2 
 |-  ( ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) -> x e. ( ( 1 / 2 ) [,] 1 ) )
18 iihalf2 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) )
19 17 18 syl 
 |-  ( ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) )
20 fvco3 
 |-  ( ( G : ( 0 [,] 1 ) --> U. J /\ ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) ) -> ( ( H o. G ) ` ( ( 2 x. x ) - 1 ) ) = ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) )
21 16 19 20 syl2an 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) ) -> ( ( H o. G ) ` ( ( 2 x. x ) - 1 ) ) = ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) )
22 21 anassrs 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( H o. G ) ` ( ( 2 x. x ) - 1 ) ) = ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) )
23 14 22 ifeq12da 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> if ( x <_ ( 1 / 2 ) , ( ( H o. F ) ` ( 2 x. x ) ) , ( ( H o. G ) ` ( ( 2 x. x ) - 1 ) ) ) = if ( x <_ ( 1 / 2 ) , ( H ` ( F ` ( 2 x. x ) ) ) , ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )
24 23 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( H o. F ) ` ( 2 x. x ) ) , ( ( H o. G ) ` ( ( 2 x. x ) - 1 ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( H ` ( F ` ( 2 x. x ) ) ) , ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
25 cnco 
 |-  ( ( F e. ( II Cn J ) /\ H e. ( J Cn K ) ) -> ( H o. F ) e. ( II Cn K ) )
26 1 4 25 syl2anc 
 |-  ( ph -> ( H o. F ) e. ( II Cn K ) )
27 cnco 
 |-  ( ( G e. ( II Cn J ) /\ H e. ( J Cn K ) ) -> ( H o. G ) e. ( II Cn K ) )
28 2 4 27 syl2anc 
 |-  ( ph -> ( H o. G ) e. ( II Cn K ) )
29 26 28 pcoval 
 |-  ( ph -> ( ( H o. F ) ( *p ` K ) ( H o. G ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( H o. F ) ` ( 2 x. x ) ) , ( ( H o. G ) ` ( ( 2 x. x ) - 1 ) ) ) ) )
30 1 2 pcoval 
 |-  ( ph -> ( F ( *p ` J ) G ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )
31 1 2 3 pcocn 
 |-  ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )
32 30 31 eqeltrrd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) e. ( II Cn J ) )
33 5 6 cnf 
 |-  ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) e. ( II Cn J ) -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) : ( 0 [,] 1 ) --> U. J )
34 32 33 syl 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) : ( 0 [,] 1 ) --> U. J )
35 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) )
36 35 fmpt 
 |-  ( A. x e. ( 0 [,] 1 ) if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) e. U. J <-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) : ( 0 [,] 1 ) --> U. J )
37 34 36 sylibr 
 |-  ( ph -> A. x e. ( 0 [,] 1 ) if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) e. U. J )
38 eqid 
 |-  U. K = U. K
39 6 38 cnf 
 |-  ( H e. ( J Cn K ) -> H : U. J --> U. K )
40 4 39 syl 
 |-  ( ph -> H : U. J --> U. K )
41 40 feqmptd 
 |-  ( ph -> H = ( y e. U. J |-> ( H ` y ) ) )
42 fveq2 
 |-  ( y = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) -> ( H ` y ) = ( H ` if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )
43 fvif 
 |-  ( H ` if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) = if ( x <_ ( 1 / 2 ) , ( H ` ( F ` ( 2 x. x ) ) ) , ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) )
44 42 43 eqtrdi 
 |-  ( y = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) -> ( H ` y ) = if ( x <_ ( 1 / 2 ) , ( H ` ( F ` ( 2 x. x ) ) ) , ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )
45 37 30 41 44 fmptcof 
 |-  ( ph -> ( H o. ( F ( *p ` J ) G ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( H ` ( F ` ( 2 x. x ) ) ) , ( H ` ( G ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
46 24 29 45 3eqtr4rd 
 |-  ( ph -> ( H o. ( F ( *p ` J ) G ) ) = ( ( H o. F ) ( *p ` K ) ( H o. G ) ) )