Metamath Proof Explorer


Theorem 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π1A
pi1co.q Q=Kπ1B
pi1co.v V=BaseP
pi1co.g G=rangVgphJFgphK
pi1co.j φJTopOnX
pi1co.f φFJCnK
pi1co.a φAX
pi1co.b φFA=B
Assertion pi1coghm φGPGrpHomQ

Proof

Step Hyp Ref Expression
1 pi1co.p P=Jπ1A
2 pi1co.q Q=Kπ1B
3 pi1co.v V=BaseP
4 pi1co.g G=rangVgphJFgphK
5 pi1co.j φJTopOnX
6 pi1co.f φFJCnK
7 pi1co.a φAX
8 pi1co.b φFA=B
9 1 pi1grp JTopOnXAXPGrp
10 5 7 9 syl2anc φPGrp
11 cntop2 FJCnKKTop
12 6 11 syl φKTop
13 toptopon2 KTopKTopOnK
14 12 13 sylib φKTopOnK
15 cnf2 JTopOnXKTopOnKFJCnKF:XK
16 5 14 6 15 syl3anc φF:XK
17 16 7 ffvelrnd φFAK
18 8 17 eqeltrrd φBK
19 2 pi1grp KTopOnKBKQGrp
20 14 18 19 syl2anc φQGrp
21 1 2 3 4 5 6 7 8 pi1cof φG:VBaseQ
22 3 a1i φV=BaseP
23 1 5 7 22 pi1bas2 φV=V/phJ
24 23 eleq2d φyVyV/phJ
25 24 biimpa φyVyV/phJ
26 eqid V/phJ=V/phJ
27 fvoveq1 fphJ=yGfphJ+Pz=Gy+Pz
28 fveq2 fphJ=yGfphJ=Gy
29 28 oveq1d fphJ=yGfphJ+QGz=Gy+QGz
30 27 29 eqeq12d fphJ=yGfphJ+Pz=GfphJ+QGzGy+Pz=Gy+QGz
31 30 ralbidv fphJ=yzVGfphJ+Pz=GfphJ+QGzzVGy+Pz=Gy+QGz
32 oveq2 hphJ=zfphJ+PhphJ=fphJ+Pz
33 32 fveq2d hphJ=zGfphJ+PhphJ=GfphJ+Pz
34 fveq2 hphJ=zGhphJ=Gz
35 34 oveq2d hphJ=zGfphJ+QGhphJ=GfphJ+QGz
36 33 35 eqeq12d hphJ=zGfphJ+PhphJ=GfphJ+QGhphJGfphJ+Pz=GfphJ+QGz
37 1 5 7 22 pi1eluni φfVfIICnJf0=Af1=A
38 37 biimpa φfVfIICnJf0=Af1=A
39 38 simp1d φfVfIICnJ
40 39 adantr φfVhVfIICnJ
41 5 adantr φfVJTopOnX
42 7 adantr φfVAX
43 3 a1i φfVV=BaseP
44 1 41 42 43 pi1eluni φfVhVhIICnJh0=Ah1=A
45 44 biimpa φfVhVhIICnJh0=Ah1=A
46 45 simp1d φfVhVhIICnJ
47 38 simp3d φfVf1=A
48 47 adantr φfVhVf1=A
49 45 simp2d φfVhVh0=A
50 48 49 eqtr4d φfVhVf1=h0
51 6 ad2antrr φfVhVFJCnK
52 40 46 50 51 copco φfVhVFf*𝑝Jh=Ff*𝑝KFh
53 52 eceq1d φfVhVFf*𝑝JhphK=Ff*𝑝KFhphK
54 40 46 50 pcocn φfVhVf*𝑝JhIICnJ
55 40 46 pco0 φfVhVf*𝑝Jh0=f0
56 38 simp2d φfVf0=A
57 56 adantr φfVhVf0=A
58 55 57 eqtrd φfVhVf*𝑝Jh0=A
59 40 46 pco1 φfVhVf*𝑝Jh1=h1
60 45 simp3d φfVhVh1=A
61 59 60 eqtrd φfVhVf*𝑝Jh1=A
62 5 ad2antrr φfVhVJTopOnX
63 7 ad2antrr φfVhVAX
64 3 a1i φfVhVV=BaseP
65 1 62 63 64 pi1eluni φfVhVf*𝑝JhVf*𝑝JhIICnJf*𝑝Jh0=Af*𝑝Jh1=A
66 54 58 61 65 mpbir3and φfVhVf*𝑝JhV
67 1 2 3 4 5 6 7 8 pi1coval φf*𝑝JhVGf*𝑝JhphJ=Ff*𝑝JhphK
68 67 adantlr φfVf*𝑝JhVGf*𝑝JhphJ=Ff*𝑝JhphK
69 66 68 syldan φfVhVGf*𝑝JhphJ=Ff*𝑝JhphK
70 eqid BaseQ=BaseQ
71 14 ad2antrr φfVhVKTopOnK
72 18 ad2antrr φfVhVBK
73 eqid +Q=+Q
74 6 adantr φfVFJCnK
75 cnco fIICnJFJCnKFfIICnK
76 39 74 75 syl2anc φfVFfIICnK
77 iitopon IITopOn01
78 cnf2 IITopOn01JTopOnXfIICnJf:01X
79 77 41 39 78 mp3an2i φfVf:01X
80 0elunit 001
81 fvco3 f:01X001Ff0=Ff0
82 79 80 81 sylancl φfVFf0=Ff0
83 56 fveq2d φfVFf0=FA
84 8 adantr φfVFA=B
85 82 83 84 3eqtrd φfVFf0=B
86 1elunit 101
87 fvco3 f:01X101Ff1=Ff1
88 79 86 87 sylancl φfVFf1=Ff1
89 47 fveq2d φfVFf1=FA
90 88 89 84 3eqtrd φfVFf1=B
91 14 adantr φfVKTopOnK
92 18 adantr φfVBK
93 eqidd φfVBaseQ=BaseQ
94 2 91 92 93 pi1eluni φfVFfBaseQFfIICnKFf0=BFf1=B
95 76 85 90 94 mpbir3and φfVFfBaseQ
96 95 adantr φfVhVFfBaseQ
97 cnco hIICnJFJCnKFhIICnK
98 46 51 97 syl2anc φfVhVFhIICnK
99 cnf2 IITopOn01JTopOnXhIICnJh:01X
100 77 62 46 99 mp3an2i φfVhVh:01X
101 fvco3 h:01X001Fh0=Fh0
102 100 80 101 sylancl φfVhVFh0=Fh0
103 49 fveq2d φfVhVFh0=FA
104 8 ad2antrr φfVhVFA=B
105 102 103 104 3eqtrd φfVhVFh0=B
106 fvco3 h:01X101Fh1=Fh1
107 100 86 106 sylancl φfVhVFh1=Fh1
108 60 fveq2d φfVhVFh1=FA
109 107 108 104 3eqtrd φfVhVFh1=B
110 eqidd φBaseQ=BaseQ
111 2 14 18 110 pi1eluni φFhBaseQFhIICnKFh0=BFh1=B
112 111 ad2antrr φfVhVFhBaseQFhIICnKFh0=BFh1=B
113 98 105 109 112 mpbir3and φfVhVFhBaseQ
114 2 70 71 72 73 96 113 pi1addval φfVhVFfphK+QFhphK=Ff*𝑝KFhphK
115 53 69 114 3eqtr4d φfVhVGf*𝑝JhphJ=FfphK+QFhphK
116 eqid +P=+P
117 simplr φfVhVfV
118 simpr φfVhVhV
119 1 3 62 63 116 117 118 pi1addval φfVhVfphJ+PhphJ=f*𝑝JhphJ
120 119 fveq2d φfVhVGfphJ+PhphJ=Gf*𝑝JhphJ
121 1 2 3 4 5 6 7 8 pi1coval φfVGfphJ=FfphK
122 121 adantr φfVhVGfphJ=FfphK
123 1 2 3 4 5 6 7 8 pi1coval φhVGhphJ=FhphK
124 123 adantlr φfVhVGhphJ=FhphK
125 122 124 oveq12d φfVhVGfphJ+QGhphJ=FfphK+QFhphK
126 115 120 125 3eqtr4d φfVhVGfphJ+PhphJ=GfphJ+QGhphJ
127 26 36 126 ectocld φfVzV/phJGfphJ+Pz=GfphJ+QGz
128 127 ralrimiva φfVzV/phJGfphJ+Pz=GfphJ+QGz
129 23 adantr φfVV=V/phJ
130 129 raleqdv φfVzVGfphJ+Pz=GfphJ+QGzzV/phJGfphJ+Pz=GfphJ+QGz
131 128 130 mpbird φfVzVGfphJ+Pz=GfphJ+QGz
132 26 31 131 ectocld φyV/phJzVGy+Pz=Gy+QGz
133 25 132 syldan φyVzVGy+Pz=Gy+QGz
134 133 ralrimiva φyVzVGy+Pz=Gy+QGz
135 21 134 jca φG:VBaseQyVzVGy+Pz=Gy+QGz
136 3 70 116 73 isghm GPGrpHomQPGrpQGrpG:VBaseQyVzVGy+Pz=Gy+QGz
137 10 20 135 136 syl21anbrc φGPGrpHomQ