Theorem reparpht

Description: Reparametrization lemma. The reparametrization of a path by any continuous map G : II --> II with G ( 0 ) = 0 and G ( 1 ) = 1 is path-homotopic to the original path. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	reparpht.1	|- ( ph -> F e. ( II Cn J ) )
	reparpht.2	|- ( ph -> G e. ( II Cn II ) )
	reparpht.3	|- ( ph -> ( G ` 0 ) = 0 )
	reparpht.4	|- ( ph -> ( G ` 1 ) = 1 )
Assertion	reparpht	|- ( ph -> ( F o. G ) ( ~=ph ` J ) F )

Proof

Step	Hyp	Ref	Expression
1		reparpht.1	|- ( ph -> F e. ( II Cn J ) )
2		reparpht.2	|- ( ph -> G e. ( II Cn II ) )
3		reparpht.3	|- ( ph -> ( G ` 0 ) = 0 )
4		reparpht.4	|- ( ph -> ( G ` 1 ) = 1 )
5		cnco	|- ( ( G e. ( II Cn II ) /\ F e. ( II Cn J ) ) -> ( F o. G ) e. ( II Cn J ) )
6	2 1 5	syl2anc	|- ( ph -> ( F o. G ) e. ( II Cn J ) )
7		eqid	|- ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) )
8	1 2 3 4 7	reparphti	|- ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) ) e. ( ( F o. G ) ( PHtpy ` J ) F ) )
9	8	ne0d	|- ( ph -> ( ( F o. G ) ( PHtpy ` J ) F ) =/= (/) )
10		isphtpc	|- ( ( F o. G ) ( ~=ph ` J ) F <-> ( ( F o. G ) e. ( II Cn J ) /\ F e. ( II Cn J ) /\ ( ( F o. G ) ( PHtpy ` J ) F ) =/= (/) ) )
11	6 1 9 10	syl3anbrc	|- ( ph -> ( F o. G ) ( ~=ph ` J ) F )