pcophtb

Description: The path homotopy equivalence relation on two paths F , G with the same start and end point can be written in terms of the loop F - G formed by concatenating F with the inverse of G . Thus, all the homotopy information in ~=phJ is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015)

	Ref	Expression
Hypotheses	pcophtb.h	$⊢ H = (x \in [0, 1] ⟼ G (1 - x))$
	pcophtb.p	$⊢ P = [0, 1] \times \{F (0)\}$
	pcophtb.f	$⊢ φ \to F \in (II Cn J)$
	pcophtb.g	$⊢ φ \to G \in (II Cn J)$
	pcophtb.0	$⊢ φ \to F (0) = G (0)$
	pcophtb.1	$⊢ φ \to F (1) = G (1)$
Assertion	pcophtb	$⊢ φ \to ((F *_{𝑝} (J) H) ≃_{ph} (J) P \leftrightarrow F ≃_{ph} (J) G)$

Proof

Step	Hyp	Ref	Expression
1		pcophtb.h	$⊢ H = (x \in [0, 1] ⟼ G (1 - x))$
2		pcophtb.p	$⊢ P = [0, 1] \times \{F (0)\}$
3		pcophtb.f	$⊢ φ \to F \in (II Cn J)$
4		pcophtb.g	$⊢ φ \to G \in (II Cn J)$
5		pcophtb.0	$⊢ φ \to F (0) = G (0)$
6		pcophtb.1	$⊢ φ \to F (1) = G (1)$
7		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
8	7	a1i	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to ≃_{ph} (J) Er (II Cn J)$
9	1	pcorevcl	$⊢ G \in (II Cn J) \to (H \in (II Cn J) \land H (0) = G (1) \land H (1) = G (0))$
10	4 9	syl	$⊢ φ \to (H \in (II Cn J) \land H (0) = G (1) \land H (1) = G (0))$
11	10	simp2d	$⊢ φ \to H (0) = G (1)$
12	6 11	eqtr4d	$⊢ φ \to F (1) = H (0)$
13	10	simp1d	$⊢ φ \to H \in (II Cn J)$
14	13 4	pco0	$⊢ φ \to (H *_{𝑝} (J) G) (0) = H (0)$
15	12 14	eqtr4d	$⊢ φ \to F (1) = (H *_{𝑝} (J) G) (0)$
16	15	adantr	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to F (1) = (H _{𝑝} (J) G) (0)$
17	3	adantr	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to F \in (II Cn J)$
18	8 17	erref	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to F ≃_{ph} (J) F$
19		eqid	$⊢ [0, 1] \times \{G (1)\} = [0, 1] \times \{G (1)\}$
20	1 19	pcorev	$⊢ G \in (II Cn J) \to (H *_{𝑝} (J) G) ≃_{ph} (J) ([0, 1] \times \{G (1)\})$
21	4 20	syl	$⊢ φ \to (H *_{𝑝} (J) G) ≃_{ph} (J) ([0, 1] \times \{G (1)\})$
22	21	adantr	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (H _{𝑝} (J) G) ≃_{ph} (J) ([0, 1] \times \{G (1)\})$
23	16 18 22	pcohtpy	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (F _{𝑝} (J) (H _{𝑝} (J) G)) ≃_{ph} (J) (F _{𝑝} (J) ([0, 1] \times \{G (1)\}))$
24	6	adantr	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to F (1) = G (1)$
25	19	pcopt2	$⊢ (F \in (II Cn J) \land F (1) = G (1)) \to (F *_{𝑝} (J) ([0, 1] \times \{G (1)\})) ≃_{ph} (J) F$
26	17 24 25	syl2anc	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (F _{𝑝} (J) ([0, 1] \times \{G (1)\})) ≃_{ph} (J) F$
27	8 23 26	ertrd	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (F _{𝑝} (J) (H *_{𝑝} (J) G)) ≃_{ph} (J) F$
28	13	adantr	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to H \in (II Cn J)$
29	4	adantr	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to G \in (II Cn J)$
30	12	adantr	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to F (1) = H (0)$
31	10	simp3d	$⊢ φ \to H (1) = G (0)$
32	31	adantr	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to H (1) = G (0)$
33		eqid	$⊢ (y \in [0, 1] ⟼ if (y \leq \frac{1}{2}, if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})), (\frac{y}{2}) + (\frac{1}{2}))) = (y \in [0, 1] ⟼ if (y \leq \frac{1}{2}, if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})), (\frac{y}{2}) + (\frac{1}{2})))$
34	17 28 29 30 32 33	pcoass	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to ((F _{𝑝} (J) H) _{𝑝} (J) G) ≃_{ph} (J) (F _{𝑝} (J) (H *_{𝑝} (J) G))$
35	3 13	pco1	$⊢ φ \to (F *_{𝑝} (J) H) (1) = H (1)$
36	35 31	eqtrd	$⊢ φ \to (F *_{𝑝} (J) H) (1) = G (0)$
37	36	adantr	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (F _{𝑝} (J) H) (1) = G (0)$
38		simpr	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (F _{𝑝} (J) H) ≃_{ph} (J) P$
39	8 29	erref	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to G ≃_{ph} (J) G$
40	37 38 39	pcohtpy	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to ((F _{𝑝} (J) H) _{𝑝} (J) G) ≃_{ph} (J) (P _{𝑝} (J) G)$
41	8 34 40	ertr3d	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (F _{𝑝} (J) (H _{𝑝} (J) G)) ≃_{ph} (J) (P _{𝑝} (J) G)$
42	5	adantr	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to F (0) = G (0)$
43	42	eqcomd	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to G (0) = F (0)$
44	2	pcopt	$⊢ (G \in (II Cn J) \land G (0) = F (0)) \to (P *_{𝑝} (J) G) ≃_{ph} (J) G$
45	29 43 44	syl2anc	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (P _{𝑝} (J) G) ≃_{ph} (J) G$
46	8 41 45	ertrd	$⊢ (φ \land (F _{𝑝} (J) H) ≃_{ph} (J) P) \to (F _{𝑝} (J) (H *_{𝑝} (J) G)) ≃_{ph} (J) G$
47	8 27 46	ertr3d	$⊢ (φ \land (F *_{𝑝} (J) H) ≃_{ph} (J) P) \to F ≃_{ph} (J) G$
48	7	a1i	$⊢ (φ \land F ≃_{ph} (J) G) \to ≃_{ph} (J) Er (II Cn J)$
49	12	adantr	$⊢ (φ \land F ≃_{ph} (J) G) \to F (1) = H (0)$
50		simpr	$⊢ (φ \land F ≃_{ph} (J) G) \to F ≃_{ph} (J) G$
51	13	adantr	$⊢ (φ \land F ≃_{ph} (J) G) \to H \in (II Cn J)$
52	48 51	erref	$⊢ (φ \land F ≃_{ph} (J) G) \to H ≃_{ph} (J) H$
53	49 50 52	pcohtpy	$⊢ (φ \land F ≃_{ph} (J) G) \to (F _{𝑝} (J) H) ≃_{ph} (J) (G _{𝑝} (J) H)$
54		eqid	$⊢ [0, 1] \times \{G (0)\} = [0, 1] \times \{G (0)\}$
55	1 54	pcorev2	$⊢ G \in (II Cn J) \to (G *_{𝑝} (J) H) ≃_{ph} (J) ([0, 1] \times \{G (0)\})$
56	4 55	syl	$⊢ φ \to (G *_{𝑝} (J) H) ≃_{ph} (J) ([0, 1] \times \{G (0)\})$
57	5	sneqd	$⊢ φ \to \{F (0)\} = \{G (0)\}$
58	57	xpeq2d	$⊢ φ \to [0, 1] \times \{F (0)\} = [0, 1] \times \{G (0)\}$
59	2 58	eqtrid	$⊢ φ \to P = [0, 1] \times \{G (0)\}$
60	56 59	breqtrrd	$⊢ φ \to (G *_{𝑝} (J) H) ≃_{ph} (J) P$
61	60	adantr	$⊢ (φ \land F ≃_{ph} (J) G) \to (G *_{𝑝} (J) H) ≃_{ph} (J) P$
62	48 53 61	ertrd	$⊢ (φ \land F ≃_{ph} (J) G) \to (F *_{𝑝} (J) H) ≃_{ph} (J) P$
63	47 62	impbida	$⊢ φ \to ((F *_{𝑝} (J) H) ≃_{ph} (J) P \leftrightarrow F ≃_{ph} (J) G)$

Metamath Proof Explorer

Theorem pcophtb

Proof