Metamath Proof Explorer

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 ⊢ φ → F ∈ II Cn J
reparpht.2 ⊢ φ → G ∈ II Cn II
reparpht.3 ⊢ φ → G ⁡ 0 = 0
reparpht.4 ⊢ φ → G ⁡ 1 = 1
Assertion reparpht ⊢ φ → F ∘ G ≃ ph ⁡ J F

Proof

Step Hyp Ref Expression
1 reparpht.1 ⊢ φ → F ∈ II Cn J
2 reparpht.2 ⊢ φ → G ∈ II Cn II
3 reparpht.3 ⊢ φ → G ⁡ 0 = 0
4 reparpht.4 ⊢ φ → G ⁡ 1 = 1
5 cnco ⊢ G ∈ II Cn II ∧ F ∈ II Cn J → F ∘ G ∈ II Cn J
6 2 1 5 syl2anc ⊢ φ → F ∘ G ∈ II Cn J
7 eqid ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ F ⁡ 1 − y ⁢ G ⁡ x + y ⁢ x = x ∈ 0 1 , y ∈ 0 1 ⟼ F ⁡ 1 − y ⁢ G ⁡ x + y ⁢ x
8 1 2 3 4 7 reparphti ⊢ φ → x ∈ 0 1 , y ∈ 0 1 ⟼ F ⁡ 1 − y ⁢ G ⁡ x + y ⁢ x ∈ F ∘ G PHtpy ⁡ J F
9 8 ne0d ⊢ φ → F ∘ G PHtpy ⁡ J F ≠ ∅
10 isphtpc ⊢ F ∘ G ≃ ph ⁡ J F ↔ F ∘ G ∈ II Cn J ∧ F ∈ II Cn J ∧ F ∘ G PHtpy ⁡ J F ≠ ∅
11 6 1 9 10 syl3anbrc ⊢ φ → F ∘ G ≃ ph ⁡ J F