Metamath Proof Explorer

Theorem pco1

Description: The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010)

Ref Expression
Hypotheses pcoval.2 
|- ( ph -> F e. ( II Cn J ) )
pcoval.3 
|- ( ph -> G e. ( II Cn J ) )
Assertion pco1 
|- ( ph -> ( ( F ( *p ` J ) G ) ` 1 ) = ( G ` 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 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 ) ) ) ) )
4 3 fveq1d 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 1 ) = ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) ` 1 ) )
5 1elunit 
 |-  1 e. ( 0 [,] 1 )
6 halflt1 
 |-  ( 1 / 2 ) < 1
7 halfre 
 |-  ( 1 / 2 ) e. RR
8 1re 
 |-  1 e. RR
9 7 8 ltnlei 
 |-  ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
10 6 9 mpbi 
 |-  -. 1 <_ ( 1 / 2 )
11 breq1 
 |-  ( x = 1 -> ( x <_ ( 1 / 2 ) <-> 1 <_ ( 1 / 2 ) ) )
12 10 11 mtbiri 
 |-  ( x = 1 -> -. x <_ ( 1 / 2 ) )
13 12 iffalsed 
 |-  ( x = 1 -> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) = ( G ` ( ( 2 x. x ) - 1 ) ) )
14 oveq2 
 |-  ( x = 1 -> ( 2 x. x ) = ( 2 x. 1 ) )
15 2t1e2 
 |-  ( 2 x. 1 ) = 2
16 14 15 eqtrdi 
 |-  ( x = 1 -> ( 2 x. x ) = 2 )
17 16 oveq1d 
 |-  ( x = 1 -> ( ( 2 x. x ) - 1 ) = ( 2 - 1 ) )
18 2m1e1 
 |-  ( 2 - 1 ) = 1
19 17 18 eqtrdi 
 |-  ( x = 1 -> ( ( 2 x. x ) - 1 ) = 1 )
20 19 fveq2d 
 |-  ( x = 1 -> ( G ` ( ( 2 x. x ) - 1 ) ) = ( G ` 1 ) )
21 13 20 eqtrd 
 |-  ( x = 1 -> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) = ( G ` 1 ) )
22 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 ) ) ) )
23 fvex 
 |-  ( G ` 1 ) e. _V
24 21 22 23 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) ` 1 ) = ( G ` 1 ) )
25 5 24 ax-mp 
 |-  ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) ` 1 ) = ( G ` 1 )
26 4 25 eqtrdi 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 1 ) = ( G ` 1 ) )