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	$⊢ φ \to F \in (II Cn J)$
	reparpht.3	$⊢ φ \to G \in (II Cn II)$
	reparpht.4	$⊢ φ \to G (0) = 0$
	reparpht.5	$⊢ φ \to G (1) = 1$
Assertion	reparpht	$⊢ φ \to (F \circ G) ≃_{ph} (J) F$

Proof

Step	Hyp	Ref	Expression
1		reparpht.2	$⊢ φ \to F \in (II Cn J)$
2		reparpht.3	$⊢ φ \to G \in (II Cn II)$
3		reparpht.4	$⊢ φ \to G (0) = 0$
4		reparpht.5	$⊢ φ \to G (1) = 1$
5		cnco	$⊢ (G \in (II Cn II) \land F \in (II Cn J)) \to F \circ G \in (II Cn J)$
6	2 1 5	syl2anc	$⊢ φ \to F \circ G \in (II Cn J)$
7		eqid	$⊢ (x \in [0, 1], y \in [0, 1] ⟼ F ((1 - y) G (x) + y x)) = (x \in [0, 1], y \in [0, 1] ⟼ F ((1 - y) G (x) + y x))$
8	1 2 3 4 7	reparphti	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ F ((1 - y) G (x) + y x)) \in ((F \circ G) PHtpy (J) F)$
9	8	ne0d	$⊢ φ \to (F \circ G) PHtpy (J) F \neq \emptyset$
10		isphtpc	$⊢ (F \circ G) ≃_{ph} (J) F \leftrightarrow (F \circ G \in (II Cn J) \land F \in (II Cn J) \land (F \circ G) PHtpy (J) F \neq \emptyset)$
11	6 1 9 10	syl3anbrc	$⊢ φ \to (F \circ G) ≃_{ph} (J) F$

Metamath Proof Explorer

Theorem reparpht

Proof