Metamath Proof Explorer

Theorem pco0

Description: The starting 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 pco0 
|- ( ph -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` 0 ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 pcoval.3 
 |-  ( ph -> G e. ( II Cn J ) )
3 0re 
 |-  0 e. RR
4 0le0 
 |-  0 <_ 0
5 halfge0 
 |-  0 <_ ( 1 / 2 )
6 halfre 
 |-  ( 1 / 2 ) e. RR
7 3 6 elicc2i 
 |-  ( 0 e. ( 0 [,] ( 1 / 2 ) ) <-> ( 0 e. RR /\ 0 <_ 0 /\ 0 <_ ( 1 / 2 ) ) )
8 3 4 5 7 mpbir3an 
 |-  0 e. ( 0 [,] ( 1 / 2 ) )
9 1 2 pcoval1 
 |-  ( ( ph /\ 0 e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` ( 2 x. 0 ) ) )
10 8 9 mpan2 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` ( 2 x. 0 ) ) )
11 2t0e0 
 |-  ( 2 x. 0 ) = 0
12 11 fveq2i 
 |-  ( F ` ( 2 x. 0 ) ) = ( F ` 0 )
13 10 12 eqtrdi 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` 0 ) )