pi1xfrcnvlem

Description: Given a path F between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	pi1xfr.p	$⊢ P = J π_{1} F (0)$
	pi1xfr.q	$⊢ Q = J π_{1} F (1)$
	pi1xfr.b	$⊢ B = {Base}_{P}$
	pi1xfr.g	$⊢ G = ran (g \in ⋃ B ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)⟩)$
	pi1xfr.j	$⊢ φ \to J \in TopOn (X)$
	pi1xfr.f	$⊢ φ \to F \in (II Cn J)$
	pi1xfr.i	$⊢ I = (x \in [0, 1] ⟼ F (1 - x))$
	pi1xfrcnv.h	$⊢ H = ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
Assertion	pi1xfrcnvlem	$⊢ φ \to G^{-1} \subseteq H$

Proof

Step	Hyp	Ref	Expression
1		pi1xfr.p	$⊢ P = J π_{1} F (0)$
2		pi1xfr.q	$⊢ Q = J π_{1} F (1)$
3		pi1xfr.b	$⊢ B = {Base}_{P}$
4		pi1xfr.g	$⊢ G = ran (g \in ⋃ B ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)⟩)$
5		pi1xfr.j	$⊢ φ \to J \in TopOn (X)$
6		pi1xfr.f	$⊢ φ \to F \in (II Cn J)$
7		pi1xfr.i	$⊢ I = (x \in [0, 1] ⟼ F (1 - x))$
8		pi1xfrcnv.h	$⊢ H = ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
9		fvex	$⊢ ≃_{ph} (J) \in V$
10		ecexg	$⊢ ≃_{ph} (J) \in V \to [g] ≃_{ph} (J) \in V$
11	9 10	mp1i	$⊢ (φ \land g \in ⋃ B) \to [g] ≃_{ph} (J) \in V$
12		ecexg	$⊢ ≃_{ph} (J) \in V \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) \in V$
13	9 12	mp1i	$⊢ (φ \land g \in ⋃ B) \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) \in V$
14	4 11 13	fliftcnv	$⊢ φ \to G^{-1} = ran (g \in ⋃ B ⟼ ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [g] ≃_{ph} (J)⟩)$
15	7	pcorevcl	$⊢ F \in (II Cn J) \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
16	6 15	syl	$⊢ φ \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
17	16	simp1d	$⊢ φ \to I \in (II Cn J)$
18	17	adantr	$⊢ (φ \land g \in ⋃ B) \to I \in (II Cn J)$
19		iitopon	$⊢ II \in TopOn ([0, 1])$
20		cnf2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land F \in (II Cn J)) \to F : [0, 1] ⟶ X$
21	19 5 6 20	mp3an2i	$⊢ φ \to F : [0, 1] ⟶ X$
22		0elunit	$⊢ 0 \in [0, 1]$
23		ffvelcdm	$⊢ (F : [0, 1] ⟶ X \land 0 \in [0, 1]) \to F (0) \in X$
24	21 22 23	sylancl	$⊢ φ \to F (0) \in X$
25	3	a1i	$⊢ φ \to B = {Base}_{P}$
26	1 5 24 25	pi1eluni	$⊢ φ \to (g \in ⋃ B \leftrightarrow (g \in (II Cn J) \land g (0) = F (0) \land g (1) = F (0)))$
27	26	biimpa	$⊢ (φ \land g \in ⋃ B) \to (g \in (II Cn J) \land g (0) = F (0) \land g (1) = F (0))$
28	27	simp1d	$⊢ (φ \land g \in ⋃ B) \to g \in (II Cn J)$
29	6	adantr	$⊢ (φ \land g \in ⋃ B) \to F \in (II Cn J)$
30	27	simp3d	$⊢ (φ \land g \in ⋃ B) \to g (1) = F (0)$
31	28 29 30	pcocn	$⊢ (φ \land g \in ⋃ B) \to g *_{𝑝} (J) F \in (II Cn J)$
32	16	simp3d	$⊢ φ \to I (1) = F (0)$
33	32	adantr	$⊢ (φ \land g \in ⋃ B) \to I (1) = F (0)$
34	27	simp2d	$⊢ (φ \land g \in ⋃ B) \to g (0) = F (0)$
35	33 34	eqtr4d	$⊢ (φ \land g \in ⋃ B) \to I (1) = g (0)$
36	28 29	pco0	$⊢ (φ \land g \in ⋃ B) \to (g *_{𝑝} (J) F) (0) = g (0)$
37	35 36	eqtr4d	$⊢ (φ \land g \in ⋃ B) \to I (1) = (g *_{𝑝} (J) F) (0)$
38	18 31 37	pcocn	$⊢ (φ \land g \in ⋃ B) \to I _{𝑝} (J) (g _{𝑝} (J) F) \in (II Cn J)$
39	18 31	pco0	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (0) = I (0)$
40	16	simp2d	$⊢ φ \to I (0) = F (1)$
41	40	adantr	$⊢ (φ \land g \in ⋃ B) \to I (0) = F (1)$
42	39 41	eqtrd	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (0) = F (1)$
43	18 31	pco1	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (1) = (g *_{𝑝} (J) F) (1)$
44	28 29	pco1	$⊢ (φ \land g \in ⋃ B) \to (g *_{𝑝} (J) F) (1) = F (1)$
45	43 44	eqtrd	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (1) = F (1)$
46		1elunit	$⊢ 1 \in [0, 1]$
47		ffvelcdm	$⊢ (F : [0, 1] ⟶ X \land 1 \in [0, 1]) \to F (1) \in X$
48	21 46 47	sylancl	$⊢ φ \to F (1) \in X$
49		eqidd	$⊢ φ \to {Base}_{Q} = {Base}_{Q}$
50	2 5 48 49	pi1eluni	$⊢ φ \to (I _{𝑝} (J) (g _{𝑝} (J) F) \in ⋃ {Base}_{Q} \leftrightarrow (I _{𝑝} (J) (g _{𝑝} (J) F) \in (II Cn J) \land (I _{𝑝} (J) (g _{𝑝} (J) F)) (0) = F (1) \land (I _{𝑝} (J) (g _{𝑝} (J) F)) (1) = F (1)))$
51	50	adantr	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F) \in ⋃ {Base}_{Q} \leftrightarrow (I _{𝑝} (J) (g _{𝑝} (J) F) \in (II Cn J) \land (I _{𝑝} (J) (g _{𝑝} (J) F)) (0) = F (1) \land (I _{𝑝} (J) (g _{𝑝} (J) F)) (1) = F (1)))$
52	38 42 45 51	mpbir3and	$⊢ (φ \land g \in ⋃ B) \to I _{𝑝} (J) (g _{𝑝} (J) F) \in ⋃ {Base}_{Q}$
53		eqidd	$⊢ φ \to (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F)) = (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F))$
54		eqidd	$⊢ φ \to (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) = (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
55		eceq1	$⊢ h = I _{𝑝} (J) (g _{𝑝} (J) F) \to [h] ≃_{ph} (J) = [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)$
56		oveq1	$⊢ h = I _{𝑝} (J) (g _{𝑝} (J) F) \to h _{𝑝} (J) I = (I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I$
57	56	oveq2d	$⊢ h = I _{𝑝} (J) (g _{𝑝} (J) F) \to F _{𝑝} (J) (h _{𝑝} (J) I) = F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I)$
58	57	eceq1d	$⊢ h = I _{𝑝} (J) (g _{𝑝} (J) F) \to [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J) = [(F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I))] ≃_{ph} (J)$
59	55 58	opeq12d	$⊢ h = I _{𝑝} (J) (g _{𝑝} (J) F) \to ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩ = ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [(F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I))] ≃_{ph} (J)⟩$
60	52 53 54 59	fmptco	$⊢ φ \to (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) \circ (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F)) = (g \in ⋃ B ⟼ ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [(F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
61		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
62	61	a1i	$⊢ (φ \land g \in ⋃ B) \to ≃_{ph} (J) Er (II Cn J)$
63	18 28	pco0	$⊢ (φ \land g \in ⋃ B) \to (I *_{𝑝} (J) g) (0) = I (0)$
64	63 41	eqtr2d	$⊢ (φ \land g \in ⋃ B) \to F (1) = (I *_{𝑝} (J) g) (0)$
65	62 29	erref	$⊢ (φ \land g \in ⋃ B) \to F ≃_{ph} (J) F$
66	62 18	erref	$⊢ (φ \land g \in ⋃ B) \to I ≃_{ph} (J) I$
67		eqid	$⊢ [0, 1] \times \{F (0)\} = [0, 1] \times \{F (0)\}$
68	67	pcopt2	$⊢ (g \in (II Cn J) \land g (1) = F (0)) \to (g *_{𝑝} (J) ([0, 1] \times \{F (0)\})) ≃_{ph} (J) g$
69	28 30 68	syl2anc	$⊢ (φ \land g \in ⋃ B) \to (g *_{𝑝} (J) ([0, 1] \times \{F (0)\})) ≃_{ph} (J) g$
70	41	eqcomd	$⊢ (φ \land g \in ⋃ B) \to F (1) = I (0)$
71		eqid	$⊢ (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})))$
72	28 29 18 30 70 71	pcoass	$⊢ (φ \land g \in ⋃ B) \to ((g _{𝑝} (J) F) _{𝑝} (J) I) ≃_{ph} (J) (g _{𝑝} (J) (F _{𝑝} (J) I))$
73	29 18	pco0	$⊢ (φ \land g \in ⋃ B) \to (F *_{𝑝} (J) I) (0) = F (0)$
74	30 73	eqtr4d	$⊢ (φ \land g \in ⋃ B) \to g (1) = (F *_{𝑝} (J) I) (0)$
75	62 28	erref	$⊢ (φ \land g \in ⋃ B) \to g ≃_{ph} (J) g$
76	7 67	pcorev2	$⊢ F \in (II Cn J) \to (F *_{𝑝} (J) I) ≃_{ph} (J) ([0, 1] \times \{F (0)\})$
77	29 76	syl	$⊢ (φ \land g \in ⋃ B) \to (F *_{𝑝} (J) I) ≃_{ph} (J) ([0, 1] \times \{F (0)\})$
78	74 75 77	pcohtpy	$⊢ (φ \land g \in ⋃ B) \to (g _{𝑝} (J) (F _{𝑝} (J) I)) ≃_{ph} (J) (g *_{𝑝} (J) ([0, 1] \times \{F (0)\}))$
79	62 72 78	ertr2d	$⊢ (φ \land g \in ⋃ B) \to (g _{𝑝} (J) ([0, 1] \times \{F (0)\})) ≃_{ph} (J) ((g _{𝑝} (J) F) *_{𝑝} (J) I)$
80	62 69 79	ertr3d	$⊢ (φ \land g \in ⋃ B) \to g ≃_{ph} (J) ((g _{𝑝} (J) F) _{𝑝} (J) I)$
81	35 66 80	pcohtpy	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) g) ≃_{ph} (J) (I _{𝑝} (J) ((g _{𝑝} (J) F) _{𝑝} (J) I))$
82	44 41	eqtr4d	$⊢ (φ \land g \in ⋃ B) \to (g *_{𝑝} (J) F) (1) = I (0)$
83	18 31 18 37 82 71	pcoass	$⊢ (φ \land g \in ⋃ B) \to ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I) ≃_{ph} (J) (I _{𝑝} (J) ((g _{𝑝} (J) F) _{𝑝} (J) I))$
84	62 81 83	ertr4d	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) g) ≃_{ph} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I)$
85	64 65 84	pcohtpy	$⊢ (φ \land g \in ⋃ B) \to (F _{𝑝} (J) (I _{𝑝} (J) g)) ≃_{ph} (J) (F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I))$
86	29 18 28 70 35 71	pcoass	$⊢ (φ \land g \in ⋃ B) \to ((F _{𝑝} (J) I) _{𝑝} (J) g) ≃_{ph} (J) (F _{𝑝} (J) (I _{𝑝} (J) g))$
87	29 18	pco1	$⊢ (φ \land g \in ⋃ B) \to (F *_{𝑝} (J) I) (1) = I (1)$
88	87 35	eqtrd	$⊢ (φ \land g \in ⋃ B) \to (F *_{𝑝} (J) I) (1) = g (0)$
89	88 77 75	pcohtpy	$⊢ (φ \land g \in ⋃ B) \to ((F _{𝑝} (J) I) _{𝑝} (J) g) ≃_{ph} (J) (([0, 1] \times \{F (0)\}) *_{𝑝} (J) g)$
90	67	pcopt	$⊢ (g \in (II Cn J) \land g (0) = F (0)) \to (([0, 1] \times \{F (0)\}) *_{𝑝} (J) g) ≃_{ph} (J) g$
91	28 34 90	syl2anc	$⊢ (φ \land g \in ⋃ B) \to (([0, 1] \times \{F (0)\}) *_{𝑝} (J) g) ≃_{ph} (J) g$
92	62 89 91	ertrd	$⊢ (φ \land g \in ⋃ B) \to ((F _{𝑝} (J) I) _{𝑝} (J) g) ≃_{ph} (J) g$
93	62 86 92	ertr3d	$⊢ (φ \land g \in ⋃ B) \to (F _{𝑝} (J) (I _{𝑝} (J) g)) ≃_{ph} (J) g$
94	62 85 93	ertr3d	$⊢ (φ \land g \in ⋃ B) \to (F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I)) ≃_{ph} (J) g$
95	62 94	erthi	$⊢ (φ \land g \in ⋃ B) \to [(F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I))] ≃_{ph} (J) = [g] ≃_{ph} (J)$
96	95	opeq2d	$⊢ (φ \land g \in ⋃ B) \to ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [(F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I))] ≃_{ph} (J)⟩ = ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [g] ≃_{ph} (J)⟩$
97	96	mpteq2dva	$⊢ φ \to (g \in ⋃ B ⟼ ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [(F _{𝑝} (J) ((I _{𝑝} (J) (g _{𝑝} (J) F)) _{𝑝} (J) I))] ≃_{ph} (J)⟩) = (g \in ⋃ B ⟼ ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [g] ≃_{ph} (J)⟩)$
98	60 97	eqtrd	$⊢ φ \to (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) \circ (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F)) = (g \in ⋃ B ⟼ ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [g] ≃_{ph} (J)⟩)$
99	98	rneqd	$⊢ φ \to ran ((h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) \circ (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F))) = ran (g \in ⋃ B ⟼ ⟨[(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J), [g] ≃_{ph} (J)⟩)$
100	14 99	eqtr4d	$⊢ φ \to G^{-1} = ran ((h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) \circ (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F)))$
101		rncoss	$⊢ ran ((h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) \circ (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F))) \subseteq ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
102	101 8	sseqtrri	$⊢ ran ((h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) \circ (g \in ⋃ B ⟼ I _{𝑝} (J) (g _{𝑝} (J) F))) \subseteq H$
103	100 102	eqsstrdi	$⊢ φ \to G^{-1} \subseteq H$

Metamath Proof Explorer

Theorem pi1xfrcnvlem

Proof