Theorem pcoval1

Description: Evaluate the concatenation of two paths on the first half. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised 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 ) )
Assertion	pcoval1	|- ( ( ph /\ X e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) G ) ` X ) = ( F ` ( 2 x. X ) ) )

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		1re	|- 1 e. RR
5		0le0	|- 0 <_ 0
6		halfre	|- ( 1 / 2 ) e. RR
7		halflt1	|- ( 1 / 2 ) < 1
8	6 4 7	ltleii	|- ( 1 / 2 ) <_ 1
9		iccss	|- ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( 0 <_ 0 /\ ( 1 / 2 ) <_ 1 ) ) -> ( 0 [,] ( 1 / 2 ) ) C_ ( 0 [,] 1 ) )
10	3 4 5 8 9	mp4an	|- ( 0 [,] ( 1 / 2 ) ) C_ ( 0 [,] 1 )
11	10	sseli	|- ( X e. ( 0 [,] ( 1 / 2 ) ) -> X e. ( 0 [,] 1 ) )
12	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 ) ) ) )
13	11 12	sylan2	|- ( ( ph /\ X e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) G ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
14		elii1	|- ( X e. ( 0 [,] ( 1 / 2 ) ) <-> ( X e. ( 0 [,] 1 ) /\ X <_ ( 1 / 2 ) ) )
15	14	simprbi	|- ( X e. ( 0 [,] ( 1 / 2 ) ) -> X <_ ( 1 / 2 ) )
16	15	iftrued	|- ( X e. ( 0 [,] ( 1 / 2 ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( F ` ( 2 x. X ) ) )
17	16	adantl	|- ( ( ph /\ X e. ( 0 [,] ( 1 / 2 ) ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( F ` ( 2 x. X ) ) )
18	13 17	eqtrd	|- ( ( ph /\ X e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) G ) ` X ) = ( F ` ( 2 x. X ) ) )