Metamath Proof Explorer

Theorem pcoval2

Description: Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010) (Proof shortened by Mario Carneiro, 7-Jun-2014)

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 ) )
Assertion pcoval2 
|- ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` 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 pcoval2.4 
 |-  ( ph -> ( F ` 1 ) = ( G ` 0 ) )
4 0re 
 |-  0 e. RR
5 1re 
 |-  1 e. RR
6 halfge0 
 |-  0 <_ ( 1 / 2 )
7 1le1 
 |-  1 <_ 1
8 iccss 
 |-  ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( 0 <_ ( 1 / 2 ) /\ 1 <_ 1 ) ) -> ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 ) )
9 4 5 6 7 8 mp4an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 )
10 9 sseli 
 |-  ( X e. ( ( 1 / 2 ) [,] 1 ) -> X e. ( 0 [,] 1 ) )
11 1 2 pcovalg 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
12 10 11 sylan2 
 |-  ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
13 3 adantr 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( F ` 1 ) = ( G ` 0 ) )
14 simprr 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> X <_ ( 1 / 2 ) )
15 halfre 
 |-  ( 1 / 2 ) e. RR
16 15 5 elicc2i 
 |-  ( X e. ( ( 1 / 2 ) [,] 1 ) <-> ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) )
17 16 simp2bi 
 |-  ( X e. ( ( 1 / 2 ) [,] 1 ) -> ( 1 / 2 ) <_ X )
18 17 ad2antrl 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( 1 / 2 ) <_ X )
19 16 simp1bi 
 |-  ( X e. ( ( 1 / 2 ) [,] 1 ) -> X e. RR )
20 19 ad2antrl 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> X e. RR )
21 letri3 
 |-  ( ( X e. RR /\ ( 1 / 2 ) e. RR ) -> ( X = ( 1 / 2 ) <-> ( X <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ X ) ) )
22 20 15 21 sylancl 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( X = ( 1 / 2 ) <-> ( X <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ X ) ) )
23 14 18 22 mpbir2and 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> X = ( 1 / 2 ) )
24 23 oveq2d 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( 2 x. X ) = ( 2 x. ( 1 / 2 ) ) )
25 2cn 
 |-  2 e. CC
26 2ne0 
 |-  2 =/= 0
27 25 26 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
28 24 27 eqtrdi 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( 2 x. X ) = 1 )
29 28 fveq2d 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( F ` ( 2 x. X ) ) = ( F ` 1 ) )
30 28 oveq1d 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( ( 2 x. X ) - 1 ) = ( 1 - 1 ) )
31 1m1e0 
 |-  ( 1 - 1 ) = 0
32 30 31 eqtrdi 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( ( 2 x. X ) - 1 ) = 0 )
33 32 fveq2d 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( G ` ( ( 2 x. X ) - 1 ) ) = ( G ` 0 ) )
34 13 29 33 3eqtr4d 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( F ` ( 2 x. X ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
35 34 ifeq1d 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = if ( X <_ ( 1 / 2 ) , ( G ` ( ( 2 x. X ) - 1 ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
36 ifid 
 |-  if ( X <_ ( 1 / 2 ) , ( G ` ( ( 2 x. X ) - 1 ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) )
37 35 36 eqtrdi 
 |-  ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
38 37 expr 
 |-  ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( X <_ ( 1 / 2 ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) ) )
39 iffalse 
 |-  ( -. X <_ ( 1 / 2 ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
40 38 39 pm2.61d1 
 |-  ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
41 12 40 eqtrd 
 |-  ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = ( G ` ( ( 2 x. X ) - 1 ) ) )