sconnpht2

Description: Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015)

	Ref	Expression
Hypotheses	sconnpht2.1	$⊢ φ \to J \in SConn$
	sconnpht2.2	$⊢ φ \to F \in (II Cn J)$
	sconnpht2.3	$⊢ φ \to G \in (II Cn J)$
	sconnpht2.4	$⊢ φ \to F (0) = G (0)$
	sconnpht2.5	$⊢ φ \to F (1) = G (1)$
Assertion	sconnpht2	$⊢ φ \to F ≃_{ph} (J) G$

Proof

Step	Hyp	Ref	Expression
1		sconnpht2.1	$⊢ φ \to J \in SConn$
2		sconnpht2.2	$⊢ φ \to F \in (II Cn J)$
3		sconnpht2.3	$⊢ φ \to G \in (II Cn J)$
4		sconnpht2.4	$⊢ φ \to F (0) = G (0)$
5		sconnpht2.5	$⊢ φ \to F (1) = G (1)$
6		eqid	$⊢ (x \in [0, 1] ⟼ G (1 - x)) = (x \in [0, 1] ⟼ G (1 - x))$
7	6	pcorevcl	$⊢ G \in (II Cn J) \to ((x \in [0, 1] ⟼ G (1 - x)) \in (II Cn J) \land (x \in [0, 1] ⟼ G (1 - x)) (0) = G (1) \land (x \in [0, 1] ⟼ G (1 - x)) (1) = G (0))$
8	3 7	syl	$⊢ φ \to ((x \in [0, 1] ⟼ G (1 - x)) \in (II Cn J) \land (x \in [0, 1] ⟼ G (1 - x)) (0) = G (1) \land (x \in [0, 1] ⟼ G (1 - x)) (1) = G (0))$
9	8	simp1d	$⊢ φ \to (x \in [0, 1] ⟼ G (1 - x)) \in (II Cn J)$
10	8	simp2d	$⊢ φ \to (x \in [0, 1] ⟼ G (1 - x)) (0) = G (1)$
11	5 10	eqtr4d	$⊢ φ \to F (1) = (x \in [0, 1] ⟼ G (1 - x)) (0)$
12	2 9 11	pcocn	$⊢ φ \to F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x)) \in (II Cn J)$
13	2 9	pco0	$⊢ φ \to (F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (0) = F (0)$
14	2 9	pco1	$⊢ φ \to (F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (1) = (x \in [0, 1] ⟼ G (1 - x)) (1)$
15	8	simp3d	$⊢ φ \to (x \in [0, 1] ⟼ G (1 - x)) (1) = G (0)$
16	4 15	eqtr4d	$⊢ φ \to F (0) = (x \in [0, 1] ⟼ G (1 - x)) (1)$
17	14 16	eqtr4d	$⊢ φ \to (F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (1) = F (0)$
18	13 17	eqtr4d	$⊢ φ \to (F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (0) = (F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (1)$
19		sconnpht	$⊢ (J \in SConn \land F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x)) \in (II Cn J) \land (F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (0) = (F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (1)) \to (F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) ≃_{ph} (J) ([0, 1] \times \{(F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (0)\})$
20	1 12 18 19	syl3anc	$⊢ φ \to (F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) ≃_{ph} (J) ([0, 1] \times \{(F _{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (0)\})$
21	13	sneqd	$⊢ φ \to \{(F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (0)\} = \{F (0)\}$
22	21	xpeq2d	$⊢ φ \to [0, 1] \times \{(F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) (0)\} = [0, 1] \times \{F (0)\}$
23	20 22	breqtrd	$⊢ φ \to (F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) ≃_{ph} (J) ([0, 1] \times \{F (0)\})$
24		eqid	$⊢ [0, 1] \times \{F (0)\} = [0, 1] \times \{F (0)\}$
25	6 24 2 3 4 5	pcophtb	$⊢ φ \to ((F *_{𝑝} (J) (x \in [0, 1] ⟼ G (1 - x))) ≃_{ph} (J) ([0, 1] \times \{F (0)\}) \leftrightarrow F ≃_{ph} (J) G)$
26	23 25	mpbid	$⊢ φ \to F ≃_{ph} (J) G$

Metamath Proof Explorer

Theorem sconnpht2

Proof