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.2	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
	reparpht.3	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn II ) )
	reparpht.4	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )
	reparpht.5	⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = 1 )
Assertion	reparpht	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ( ≃ph ‘ 𝐽 ) 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		reparpht.2	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2		reparpht.3	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn II ) )
3		reparpht.4	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )
4		reparpht.5	⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = 1 )
5		cnco	⊢ ( ( 𝐺 ∈ ( II Cn II ) ∧ 𝐹 ∈ ( II Cn 𝐽 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( II Cn 𝐽 ) )
6	2 1 5	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ ( II Cn 𝐽 ) )
7		eqid	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( ( ( 1 − 𝑦 ) · ( 𝐺 ‘ 𝑥 ) ) + ( 𝑦 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( ( ( 1 − 𝑦 ) · ( 𝐺 ‘ 𝑥 ) ) + ( 𝑦 · 𝑥 ) ) ) )
8	1 2 3 4 7	reparphti	⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( ( ( 1 − 𝑦 ) · ( 𝐺 ‘ 𝑥 ) ) + ( 𝑦 · 𝑥 ) ) ) ) ∈ ( ( 𝐹 ∘ 𝐺 ) ( PHtpy ‘ 𝐽 ) 𝐹 ) )
9	8	ne0d	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ( PHtpy ‘ 𝐽 ) 𝐹 ) ≠ ∅ )
10		isphtpc	⊢ ( ( 𝐹 ∘ 𝐺 ) ( ≃ph ‘ 𝐽 ) 𝐹 ↔ ( ( 𝐹 ∘ 𝐺 ) ∈ ( II Cn 𝐽 ) ∧ 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐹 ∘ 𝐺 ) ( PHtpy ‘ 𝐽 ) 𝐹 ) ≠ ∅ ) )
11	6 1 9 10	syl3anbrc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ( ≃ph ‘ 𝐽 ) 𝐹 )