pi1xfrcnv

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	pi1xfrcnv	$⊢ φ \to (G^{-1} = H \land G^{-1} \in (Q GrpHom P))$

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	1 2 3 4 5 6 7 8	pi1xfrcnvlem	$⊢ φ \to G^{-1} \subseteq H$
10		fvex	$⊢ ≃_{ph} (J) \in V$
11		ecexg	$⊢ ≃_{ph} (J) \in V \to [h] ≃_{ph} (J) \in V$
12	10 11	mp1i	$⊢ (φ \land h \in ⋃ {Base}_{Q}) \to [h] ≃_{ph} (J) \in V$
13		ecexg	$⊢ ≃_{ph} (J) \in V \to [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J) \in V$
14	10 13	mp1i	$⊢ (φ \land h \in ⋃ {Base}_{Q}) \to [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J) \in V$
15	8 12 14	fliftrel	$⊢ φ \to H \subseteq V \times V$
16		df-rel	$⊢ Rel H \leftrightarrow H \subseteq V \times V$
17	15 16	sylibr	$⊢ φ \to Rel H$
18		dfrel2	$⊢ Rel H \leftrightarrow {H^{-1}}^{-1} = H$
19	17 18	sylib	$⊢ φ \to {H^{-1}}^{-1} = H$
20		0elunit	$⊢ 0 \in [0, 1]$
21		oveq2	$⊢ x = 0 \to 1 - x = 1 - 0$
22		1m0e1	$⊢ 1 - 0 = 1$
23	21 22	syl6eq	$⊢ x = 0 \to 1 - x = 1$
24	23	fveq2d	$⊢ x = 0 \to F (1 - x) = F (1)$
25		fvex	$⊢ F (1) \in V$
26	24 7 25	fvmpt	$⊢ 0 \in [0, 1] \to I (0) = F (1)$
27	20 26	ax-mp	$⊢ I (0) = F (1)$
28	27	oveq2i	$⊢ J π_{1} I (0) = J π_{1} F (1)$
29	2 28	eqtr4i	$⊢ Q = J π_{1} I (0)$
30		1elunit	$⊢ 1 \in [0, 1]$
31		oveq2	$⊢ x = 1 \to 1 - x = 1 - 1$
32	31	fveq2d	$⊢ x = 1 \to F (1 - x) = F (1 - 1)$
33		1m1e0	$⊢ 1 - 1 = 0$
34	33	fveq2i	$⊢ F (1 - 1) = F (0)$
35	32 34	syl6eq	$⊢ x = 1 \to F (1 - x) = F (0)$
36		fvex	$⊢ F (0) \in V$
37	35 7 36	fvmpt	$⊢ 1 \in [0, 1] \to I (1) = F (0)$
38	30 37	ax-mp	$⊢ I (1) = F (0)$
39	38	oveq2i	$⊢ J π_{1} I (1) = J π_{1} F (0)$
40	1 39	eqtr4i	$⊢ P = J π_{1} I (1)$
41		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
42		eqid	$⊢ ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) = ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
43	7	pcorevcl	$⊢ F \in (II Cn J) \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
44	6 43	syl	$⊢ φ \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
45	44	simp1d	$⊢ φ \to I \in (II Cn J)$
46		oveq2	$⊢ z = y \to 1 - z = 1 - y$
47	46	fveq2d	$⊢ z = y \to I (1 - z) = I (1 - y)$
48	47	cbvmptv	$⊢ (z \in [0, 1] ⟼ I (1 - z)) = (y \in [0, 1] ⟼ I (1 - y))$
49		eqid	$⊢ ran (g \in ⋃ {Base}_{P} ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)⟩) = ran (g \in ⋃ {Base}_{P} ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)⟩)$
50	29 40 41 42 5 45 48 49	pi1xfrcnvlem	$⊢ φ \to {ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)}^{-1} \subseteq ran (g \in ⋃ {Base}_{P} ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)⟩)$
51		iitopon	$⊢ II \in TopOn ([0, 1])$
52		cnf2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land F \in (II Cn J)) \to F : [0, 1] ⟶ X$
53	51 5 6 52	mp3an2i	$⊢ φ \to F : [0, 1] ⟶ X$
54	53	feqmptd	$⊢ φ \to F = (z \in [0, 1] ⟼ F (z))$
55		iirev	$⊢ z \in [0, 1] \to 1 - z \in [0, 1]$
56		oveq2	$⊢ x = 1 - z \to 1 - x = 1 - (1 - z)$
57	56	fveq2d	$⊢ x = 1 - z \to F (1 - x) = F (1 - (1 - z))$
58		fvex	$⊢ F (1 - (1 - z)) \in V$
59	57 7 58	fvmpt	$⊢ 1 - z \in [0, 1] \to I (1 - z) = F (1 - (1 - z))$
60	55 59	syl	$⊢ z \in [0, 1] \to I (1 - z) = F (1 - (1 - z))$
61		ax-1cn	$⊢ 1 \in ℂ$
62		unitssre	$⊢ [0, 1] \subseteq ℝ$
63	62	sseli	$⊢ z \in [0, 1] \to z \in ℝ$
64	63	recnd	$⊢ z \in [0, 1] \to z \in ℂ$
65		nncan	$⊢ (1 \in ℂ \land z \in ℂ) \to 1 - (1 - z) = z$
66	61 64 65	sylancr	$⊢ z \in [0, 1] \to 1 - (1 - z) = z$
67	66	fveq2d	$⊢ z \in [0, 1] \to F (1 - (1 - z)) = F (z)$
68	60 67	eqtrd	$⊢ z \in [0, 1] \to I (1 - z) = F (z)$
69	68	mpteq2ia	$⊢ (z \in [0, 1] ⟼ I (1 - z)) = (z \in [0, 1] ⟼ F (z))$
70	54 69	syl6eqr	$⊢ φ \to F = (z \in [0, 1] ⟼ I (1 - z))$
71	70	oveq1d	$⊢ φ \to F _{𝑝} (J) (h _{𝑝} (J) I) = (z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I)$
72	71	eceq1d	$⊢ φ \to [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J) = [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)$
73	72	opeq2d	$⊢ φ \to ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩ = ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩$
74	73	mpteq2dv	$⊢ φ \to (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) = (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
75	74	rneqd	$⊢ φ \to ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [(F _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) = ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
76	8 75	syl5eq	$⊢ φ \to H = ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
77	76	cnveqd	$⊢ φ \to H^{-1} = {ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)}^{-1}$
78	3	a1i	$⊢ φ \to B = {Base}_{P}$
79	78	unieqd	$⊢ φ \to ⋃ B = ⋃ {Base}_{P}$
80	70	oveq2d	$⊢ φ \to g _{𝑝} (J) F = g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))$
81	80	oveq2d	$⊢ φ \to I _{𝑝} (J) (g _{𝑝} (J) F) = I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z)))$
82	81	eceq1d	$⊢ φ \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) = [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)$
83	82	opeq2d	$⊢ φ \to ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)⟩ = ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)⟩$
84	79 83	mpteq12dv	$⊢ φ \to (g \in ⋃ B ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)⟩) = (g \in ⋃ {Base}_{P} ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)⟩)$
85	84	rneqd	$⊢ φ \to ran (g \in ⋃ B ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)⟩) = ran (g \in ⋃ {Base}_{P} ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)⟩)$
86	4 85	syl5eq	$⊢ φ \to G = ran (g \in ⋃ {Base}_{P} ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) (z \in [0, 1] ⟼ I (1 - z))))] ≃_{ph} (J)⟩)$
87	50 77 86	3sstr4d	$⊢ φ \to H^{-1} \subseteq G$
88		cnvss	$⊢ H^{-1} \subseteq G \to {H^{-1}}^{-1} \subseteq G^{-1}$
89	87 88	syl	$⊢ φ \to {H^{-1}}^{-1} \subseteq G^{-1}$
90	19 89	eqsstrrd	$⊢ φ \to H \subseteq G^{-1}$
91	9 90	eqssd	$⊢ φ \to G^{-1} = H$
92	91 76	eqtrd	$⊢ φ \to G^{-1} = ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩)$
93	29 40 41 42 5 45 48	pi1xfr	$⊢ φ \to ran (h \in ⋃ {Base}_{Q} ⟼ ⟨[h] ≃_{ph} (J), [((z \in [0, 1] ⟼ I (1 - z)) _{𝑝} (J) (h _{𝑝} (J) I))] ≃_{ph} (J)⟩) \in (Q GrpHom P)$
94	92 93	eqeltrd	$⊢ φ \to G^{-1} \in (Q GrpHom P)$
95	91 94	jca	$⊢ φ \to (G^{-1} = H \land G^{-1} \in (Q GrpHom P))$

Metamath Proof Explorer

Theorem pi1xfrcnv

Proof