Metamath Proof Explorer

Theorem pcoval

Description: The concatenation of two paths. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses pcoval.2 
|- ( ph -> F e. ( II Cn J ) )
pcoval.3 
|- ( ph -> G e. ( II Cn J ) )
Assertion pcoval 
|- ( ph -> ( F ( *p ` J ) G ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 pcoval.3 
 |-  ( ph -> G e. ( II Cn J ) )
3 fveq1 
 |-  ( f = F -> ( f ` ( 2 x. x ) ) = ( F ` ( 2 x. x ) ) )
4 3 adantr 
 |-  ( ( f = F /\ g = G ) -> ( f ` ( 2 x. x ) ) = ( F ` ( 2 x. x ) ) )
5 fveq1 
 |-  ( g = G -> ( g ` ( ( 2 x. x ) - 1 ) ) = ( G ` ( ( 2 x. x ) - 1 ) ) )
6 5 adantl 
 |-  ( ( f = F /\ g = G ) -> ( g ` ( ( 2 x. x ) - 1 ) ) = ( G ` ( ( 2 x. x ) - 1 ) ) )
7 4 6 ifeq12d 
 |-  ( ( f = F /\ g = G ) -> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) )
8 7 mpteq2dv 
 |-  ( ( f = F /\ g = G ) -> ( 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 ) ) ) ) )
9 pcofval 
 |-  ( *p ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) )
10 ovex 
 |-  ( 0 [,] 1 ) e. _V
11 10 mptex 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) e. _V
12 8 9 11 ovmpoa 
 |-  ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) -> ( F ( *p ` J ) G ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )
13 1 2 12 syl2anc 
 |-  ( ph -> ( F ( *p ` J ) G ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )