Theorem pcorev

Description: Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

	Ref	Expression
Hypotheses	pcorev.1	|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
	pcorev.2	|- P = ( ( 0 [,] 1 ) X. { ( F ` 1 ) } )
Assertion	pcorev	|- ( F e. ( II Cn J ) -> ( G ( *p ` J ) F ) ( ~=ph ` J ) P )

Proof

Step	Hyp	Ref	Expression
1		pcorev.1	|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
2		pcorev.2	|- P = ( ( 0 [,] 1 ) X. { ( F ` 1 ) } )
3		eqid	|- ( s e. ( 0 [,] 1 ) , t e. ( 0 [,] 1 ) |-> ( F ` if ( s <_ ( 1 / 2 ) , ( 1 - ( ( 1 - t ) x. ( 2 x. s ) ) ) , ( 1 - ( ( 1 - t ) x. ( 1 - ( ( 2 x. s ) - 1 ) ) ) ) ) ) ) = ( s e. ( 0 [,] 1 ) , t e. ( 0 [,] 1 ) |-> ( F ` if ( s <_ ( 1 / 2 ) , ( 1 - ( ( 1 - t ) x. ( 2 x. s ) ) ) , ( 1 - ( ( 1 - t ) x. ( 1 - ( ( 2 x. s ) - 1 ) ) ) ) ) ) )
4	1 2 3	pcorevlem	|- ( F e. ( II Cn J ) -> ( ( s e. ( 0 [,] 1 ) , t e. ( 0 [,] 1 ) |-> ( F ` if ( s <_ ( 1 / 2 ) , ( 1 - ( ( 1 - t ) x. ( 2 x. s ) ) ) , ( 1 - ( ( 1 - t ) x. ( 1 - ( ( 2 x. s ) - 1 ) ) ) ) ) ) ) e. ( ( G ( *p ` J ) F ) ( PHtpy ` J ) P ) /\ ( G ( *p ` J ) F ) ( ~=ph ` J ) P ) )
5	4	simprd	|- ( F e. ( II Cn J ) -> ( G ( *p ` J ) F ) ( ~=ph ` J ) P )