pi1coghm

Description: The mapping G between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015) (Revised by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	pi1co.p	$⊢ P = J π_{1} A$
	pi1co.q	$⊢ Q = K π_{1} B$
	pi1co.v	$⊢ V = {Base}_{P}$
	pi1co.g	$⊢ G = ran (g \in ⋃ V ⟼ ⟨[g] ≃_{ph} (J), [(F \circ g)] ≃_{ph} (K)⟩)$
	pi1co.j	$⊢ φ \to J \in TopOn (X)$
	pi1co.f	$⊢ φ \to F \in (J Cn K)$
	pi1co.a	$⊢ φ \to A \in X$
	pi1co.b	$⊢ φ \to F (A) = B$
Assertion	pi1coghm	$⊢ φ \to G \in (P GrpHom Q)$

Proof

Step	Hyp	Ref	Expression
1		pi1co.p	$⊢ P = J π_{1} A$
2		pi1co.q	$⊢ Q = K π_{1} B$
3		pi1co.v	$⊢ V = {Base}_{P}$
4		pi1co.g	$⊢ G = ran (g \in ⋃ V ⟼ ⟨[g] ≃_{ph} (J), [(F \circ g)] ≃_{ph} (K)⟩)$
5		pi1co.j	$⊢ φ \to J \in TopOn (X)$
6		pi1co.f	$⊢ φ \to F \in (J Cn K)$
7		pi1co.a	$⊢ φ \to A \in X$
8		pi1co.b	$⊢ φ \to F (A) = B$
9	1	pi1grp	$⊢ (J \in TopOn (X) \land A \in X) \to P \in Grp$
10	5 7 9	syl2anc	$⊢ φ \to P \in Grp$
11		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
12	6 11	syl	$⊢ φ \to K \in Top$
13		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
14	12 13	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
15		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (⋃ K) \land F \in (J Cn K)) \to F : X ⟶ ⋃ K$
16	5 14 6 15	syl3anc	$⊢ φ \to F : X ⟶ ⋃ K$
17	16 7	ffvelrnd	$⊢ φ \to F (A) \in ⋃ K$
18	8 17	eqeltrrd	$⊢ φ \to B \in ⋃ K$
19	2	pi1grp	$⊢ (K \in TopOn (⋃ K) \land B \in ⋃ K) \to Q \in Grp$
20	14 18 19	syl2anc	$⊢ φ \to Q \in Grp$
21	1 2 3 4 5 6 7 8	pi1cof	$⊢ φ \to G : V ⟶ {Base}_{Q}$
22	3	a1i	$⊢ φ \to V = {Base}_{P}$
23	1 5 7 22	pi1bas2	$⊢ φ \to V = ⋃ V / ≃_{ph} (J)$
24	23	eleq2d	$⊢ φ \to (y \in V \leftrightarrow y \in (⋃ V / ≃_{ph} (J)))$
25	24	biimpa	$⊢ (φ \land y \in V) \to y \in (⋃ V / ≃_{ph} (J))$
26		eqid	$⊢ ⋃ V / ≃_{ph} (J) = ⋃ V / ≃_{ph} (J)$
27		fvoveq1	$⊢ [f] ≃_{ph} (J) = y \to G ([f] ≃_{ph} (J) +_{P} z) = G (y +_{P} z)$
28		fveq2	$⊢ [f] ≃_{ph} (J) = y \to G ([f] ≃_{ph} (J)) = G (y)$
29	28	oveq1d	$⊢ [f] ≃_{ph} (J) = y \to G ([f] ≃_{ph} (J)) +_{Q} G (z) = G (y) +_{Q} G (z)$
30	27 29	eqeq12d	$⊢ [f] ≃_{ph} (J) = y \to (G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z) \leftrightarrow G (y +_{P} z) = G (y) +_{Q} G (z))$
31	30	ralbidv	$⊢ [f] ≃_{ph} (J) = y \to (\forall z \in V G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z) \leftrightarrow \forall z \in V G (y +_{P} z) = G (y) +_{Q} G (z))$
32		oveq2	$⊢ [h] ≃_{ph} (J) = z \to [f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J) = [f] ≃_{ph} (J) +_{P} z$
33	32	fveq2d	$⊢ [h] ≃_{ph} (J) = z \to G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J) +_{P} z)$
34		fveq2	$⊢ [h] ≃_{ph} (J) = z \to G ([h] ≃_{ph} (J)) = G (z)$
35	34	oveq2d	$⊢ [h] ≃_{ph} (J) = z \to G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
36	33 35	eqeq12d	$⊢ [h] ≃_{ph} (J) = z \to (G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J)) \leftrightarrow G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z))$
37	1 5 7 22	pi1eluni	$⊢ φ \to (f \in ⋃ V \leftrightarrow (f \in (II Cn J) \land f (0) = A \land f (1) = A))$
38	37	biimpa	$⊢ (φ \land f \in ⋃ V) \to (f \in (II Cn J) \land f (0) = A \land f (1) = A)$
39	38	simp1d	$⊢ (φ \land f \in ⋃ V) \to f \in (II Cn J)$
40	39	adantr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to f \in (II Cn J)$
41	5	adantr	$⊢ (φ \land f \in ⋃ V) \to J \in TopOn (X)$
42	7	adantr	$⊢ (φ \land f \in ⋃ V) \to A \in X$
43	3	a1i	$⊢ (φ \land f \in ⋃ V) \to V = {Base}_{P}$
44	1 41 42 43	pi1eluni	$⊢ (φ \land f \in ⋃ V) \to (h \in ⋃ V \leftrightarrow (h \in (II Cn J) \land h (0) = A \land h (1) = A))$
45	44	biimpa	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (h \in (II Cn J) \land h (0) = A \land h (1) = A)$
46	45	simp1d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to h \in (II Cn J)$
47	38	simp3d	$⊢ (φ \land f \in ⋃ V) \to f (1) = A$
48	47	adantr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to f (1) = A$
49	45	simp2d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to h (0) = A$
50	48 49	eqtr4d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to f (1) = h (0)$
51	6	ad2antrr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F \in (J Cn K)$
52	40 46 50 51	copco	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F \circ (f _{𝑝} (J) h) = (F \circ f) _{𝑝} (K) (F \circ h)$
53	52	eceq1d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to [(F \circ (f _{𝑝} (J) h))] ≃_{ph} (K) = [((F \circ f) _{𝑝} (K) (F \circ h))] ≃_{ph} (K)$
54	40 46 50	pcocn	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to f *_{𝑝} (J) h \in (II Cn J)$
55	40 46	pco0	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (f *_{𝑝} (J) h) (0) = f (0)$
56	38	simp2d	$⊢ (φ \land f \in ⋃ V) \to f (0) = A$
57	56	adantr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to f (0) = A$
58	55 57	eqtrd	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (f *_{𝑝} (J) h) (0) = A$
59	40 46	pco1	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (f *_{𝑝} (J) h) (1) = h (1)$
60	45	simp3d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to h (1) = A$
61	59 60	eqtrd	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (f *_{𝑝} (J) h) (1) = A$
62	5	ad2antrr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to J \in TopOn (X)$
63	7	ad2antrr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to A \in X$
64	3	a1i	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to V = {Base}_{P}$
65	1 62 63 64	pi1eluni	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (f _{𝑝} (J) h \in ⋃ V \leftrightarrow (f _{𝑝} (J) h \in (II Cn J) \land (f _{𝑝} (J) h) (0) = A \land (f _{𝑝} (J) h) (1) = A))$
66	54 58 61 65	mpbir3and	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to f *_{𝑝} (J) h \in ⋃ V$
67	1 2 3 4 5 6 7 8	pi1coval	$⊢ (φ \land f _{𝑝} (J) h \in ⋃ V) \to G ([(f _{𝑝} (J) h)] ≃_{ph} (J)) = [(F \circ (f *_{𝑝} (J) h))] ≃_{ph} (K)$
68	67	adantlr	$⊢ ((φ \land f \in ⋃ V) \land f _{𝑝} (J) h \in ⋃ V) \to G ([(f _{𝑝} (J) h)] ≃_{ph} (J)) = [(F \circ (f *_{𝑝} (J) h))] ≃_{ph} (K)$
69	66 68	syldan	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to G ([(f _{𝑝} (J) h)] ≃_{ph} (J)) = [(F \circ (f _{𝑝} (J) h))] ≃_{ph} (K)$
70		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
71	14	ad2antrr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to K \in TopOn (⋃ K)$
72	18	ad2antrr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to B \in ⋃ K$
73		eqid	$⊢ +_{Q} = +_{Q}$
74	6	adantr	$⊢ (φ \land f \in ⋃ V) \to F \in (J Cn K)$
75		cnco	$⊢ (f \in (II Cn J) \land F \in (J Cn K)) \to F \circ f \in (II Cn K)$
76	39 74 75	syl2anc	$⊢ (φ \land f \in ⋃ V) \to F \circ f \in (II Cn K)$
77		iitopon	$⊢ II \in TopOn ([0, 1])$
78		cnf2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land f \in (II Cn J)) \to f : [0, 1] ⟶ X$
79	77 41 39 78	mp3an2i	$⊢ (φ \land f \in ⋃ V) \to f : [0, 1] ⟶ X$
80		0elunit	$⊢ 0 \in [0, 1]$
81		fvco3	$⊢ (f : [0, 1] ⟶ X \land 0 \in [0, 1]) \to (F \circ f) (0) = F (f (0))$
82	79 80 81	sylancl	$⊢ (φ \land f \in ⋃ V) \to (F \circ f) (0) = F (f (0))$
83	56	fveq2d	$⊢ (φ \land f \in ⋃ V) \to F (f (0)) = F (A)$
84	8	adantr	$⊢ (φ \land f \in ⋃ V) \to F (A) = B$
85	82 83 84	3eqtrd	$⊢ (φ \land f \in ⋃ V) \to (F \circ f) (0) = B$
86		1elunit	$⊢ 1 \in [0, 1]$
87		fvco3	$⊢ (f : [0, 1] ⟶ X \land 1 \in [0, 1]) \to (F \circ f) (1) = F (f (1))$
88	79 86 87	sylancl	$⊢ (φ \land f \in ⋃ V) \to (F \circ f) (1) = F (f (1))$
89	47	fveq2d	$⊢ (φ \land f \in ⋃ V) \to F (f (1)) = F (A)$
90	88 89 84	3eqtrd	$⊢ (φ \land f \in ⋃ V) \to (F \circ f) (1) = B$
91	14	adantr	$⊢ (φ \land f \in ⋃ V) \to K \in TopOn (⋃ K)$
92	18	adantr	$⊢ (φ \land f \in ⋃ V) \to B \in ⋃ K$
93		eqidd	$⊢ (φ \land f \in ⋃ V) \to {Base}_{Q} = {Base}_{Q}$
94	2 91 92 93	pi1eluni	$⊢ (φ \land f \in ⋃ V) \to (F \circ f \in ⋃ {Base}_{Q} \leftrightarrow (F \circ f \in (II Cn K) \land (F \circ f) (0) = B \land (F \circ f) (1) = B))$
95	76 85 90 94	mpbir3and	$⊢ (φ \land f \in ⋃ V) \to F \circ f \in ⋃ {Base}_{Q}$
96	95	adantr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F \circ f \in ⋃ {Base}_{Q}$
97		cnco	$⊢ (h \in (II Cn J) \land F \in (J Cn K)) \to F \circ h \in (II Cn K)$
98	46 51 97	syl2anc	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F \circ h \in (II Cn K)$
99		cnf2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land h \in (II Cn J)) \to h : [0, 1] ⟶ X$
100	77 62 46 99	mp3an2i	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to h : [0, 1] ⟶ X$
101		fvco3	$⊢ (h : [0, 1] ⟶ X \land 0 \in [0, 1]) \to (F \circ h) (0) = F (h (0))$
102	100 80 101	sylancl	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (F \circ h) (0) = F (h (0))$
103	49	fveq2d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F (h (0)) = F (A)$
104	8	ad2antrr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F (A) = B$
105	102 103 104	3eqtrd	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (F \circ h) (0) = B$
106		fvco3	$⊢ (h : [0, 1] ⟶ X \land 1 \in [0, 1]) \to (F \circ h) (1) = F (h (1))$
107	100 86 106	sylancl	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (F \circ h) (1) = F (h (1))$
108	60	fveq2d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F (h (1)) = F (A)$
109	107 108 104	3eqtrd	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (F \circ h) (1) = B$
110		eqidd	$⊢ φ \to {Base}_{Q} = {Base}_{Q}$
111	2 14 18 110	pi1eluni	$⊢ φ \to (F \circ h \in ⋃ {Base}_{Q} \leftrightarrow (F \circ h \in (II Cn K) \land (F \circ h) (0) = B \land (F \circ h) (1) = B))$
112	111	ad2antrr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to (F \circ h \in ⋃ {Base}_{Q} \leftrightarrow (F \circ h \in (II Cn K) \land (F \circ h) (0) = B \land (F \circ h) (1) = B))$
113	98 105 109 112	mpbir3and	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to F \circ h \in ⋃ {Base}_{Q}$
114	2 70 71 72 73 96 113	pi1addval	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to [(F \circ f)] ≃_{ph} (K) +_{Q} [(F \circ h)] ≃_{ph} (K) = [((F \circ f) *_{𝑝} (K) (F \circ h))] ≃_{ph} (K)$
115	53 69 114	3eqtr4d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to G ([(f *_{𝑝} (J) h)] ≃_{ph} (J)) = [(F \circ f)] ≃_{ph} (K) +_{Q} [(F \circ h)] ≃_{ph} (K)$
116		eqid	$⊢ +_{P} = +_{P}$
117		simplr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to f \in ⋃ V$
118		simpr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to h \in ⋃ V$
119	1 3 62 63 116 117 118	pi1addval	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to [f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J) = [(f *_{𝑝} (J) h)] ≃_{ph} (J)$
120	119	fveq2d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([(f *_{𝑝} (J) h)] ≃_{ph} (J))$
121	1 2 3 4 5 6 7 8	pi1coval	$⊢ (φ \land f \in ⋃ V) \to G ([f] ≃_{ph} (J)) = [(F \circ f)] ≃_{ph} (K)$
122	121	adantr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to G ([f] ≃_{ph} (J)) = [(F \circ f)] ≃_{ph} (K)$
123	1 2 3 4 5 6 7 8	pi1coval	$⊢ (φ \land h \in ⋃ V) \to G ([h] ≃_{ph} (J)) = [(F \circ h)] ≃_{ph} (K)$
124	123	adantlr	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to G ([h] ≃_{ph} (J)) = [(F \circ h)] ≃_{ph} (K)$
125	122 124	oveq12d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J)) = [(F \circ f)] ≃_{ph} (K) +_{Q} [(F \circ h)] ≃_{ph} (K)$
126	115 120 125	3eqtr4d	$⊢ ((φ \land f \in ⋃ V) \land h \in ⋃ V) \to G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J))$
127	26 36 126	ectocld	$⊢ ((φ \land f \in ⋃ V) \land z \in (⋃ V / ≃_{ph} (J))) \to G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
128	127	ralrimiva	$⊢ (φ \land f \in ⋃ V) \to \forall z \in (⋃ V / ≃_{ph} (J)) G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
129	23	adantr	$⊢ (φ \land f \in ⋃ V) \to V = ⋃ V / ≃_{ph} (J)$
130	129	raleqdv	$⊢ (φ \land f \in ⋃ V) \to (\forall z \in V G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z) \leftrightarrow \forall z \in (⋃ V / ≃_{ph} (J)) G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z))$
131	128 130	mpbird	$⊢ (φ \land f \in ⋃ V) \to \forall z \in V G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
132	26 31 131	ectocld	$⊢ (φ \land y \in (⋃ V / ≃_{ph} (J))) \to \forall z \in V G (y +_{P} z) = G (y) +_{Q} G (z)$
133	25 132	syldan	$⊢ (φ \land y \in V) \to \forall z \in V G (y +_{P} z) = G (y) +_{Q} G (z)$
134	133	ralrimiva	$⊢ φ \to \forall y \in V \forall z \in V G (y +_{P} z) = G (y) +_{Q} G (z)$
135	21 134	jca	$⊢ φ \to (G : V ⟶ {Base}_{Q} \land \forall y \in V \forall z \in V G (y +_{P} z) = G (y) +_{Q} G (z))$
136	3 70 116 73	isghm	$⊢ G \in (P GrpHom Q) \leftrightarrow ((P \in Grp \land Q \in Grp) \land (G : V ⟶ {Base}_{Q} \land \forall y \in V \forall z \in V G (y +_{P} z) = G (y) +_{Q} G (z)))$
137	10 20 135 136	syl21anbrc	$⊢ φ \to G \in (P GrpHom Q)$

Metamath Proof Explorer

Theorem pi1coghm

Proof