Theorem pcovalg

Description: Evaluate the concatenation of two paths. (Contributed 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	pcovalg	|- ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = 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	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 ) ` X ) = ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) ` X ) )
5		breq1	|- ( x = X -> ( x <_ ( 1 / 2 ) <-> X <_ ( 1 / 2 ) ) )
6		oveq2	|- ( x = X -> ( 2 x. x ) = ( 2 x. X ) )
7	6	fveq2d	|- ( x = X -> ( F ` ( 2 x. x ) ) = ( F ` ( 2 x. X ) ) )
8	6	fvoveq1d	|- ( x = X -> ( G ` ( ( 2 x. x ) - 1 ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
9	5 7 8	ifbieq12d	|- ( x = X -> 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 ) ) ) )
10		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 ) ) ) )
11		fvex	|- ( F ` ( 2 x. X ) ) e. _V
12		fvex	|- ( G ` ( ( 2 x. X ) - 1 ) ) e. _V
13	11 12	ifex	|- if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) e. _V
14	9 10 13	fvmpt	|- ( X e. ( 0 [,] 1 ) -> ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
15	4 14	sylan9eq	|- ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )