Metamath Proof Explorer


Theorem tgpconncomp

Description: The identity component, the connected component containing the identity element, is a closed ( conncompcld ) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypotheses tgpconncomp.x X=BaseG
tgpconncomp.z 0˙=0G
tgpconncomp.j J=TopOpenG
tgpconncomp.s S=x𝒫X|0˙xJ𝑡xConn
Assertion tgpconncomp GTopGrpSNrmSGrpG

Proof

Step Hyp Ref Expression
1 tgpconncomp.x X=BaseG
2 tgpconncomp.z 0˙=0G
3 tgpconncomp.j J=TopOpenG
4 tgpconncomp.s S=x𝒫X|0˙xJ𝑡xConn
5 ssrab2 x𝒫X|0˙xJ𝑡xConn𝒫X
6 sspwuni x𝒫X|0˙xJ𝑡xConn𝒫Xx𝒫X|0˙xJ𝑡xConnX
7 5 6 mpbi x𝒫X|0˙xJ𝑡xConnX
8 4 7 eqsstri SX
9 8 a1i GTopGrpSX
10 3 1 tgptopon GTopGrpJTopOnX
11 tgpgrp GTopGrpGGrp
12 1 2 grpidcl GGrp0˙X
13 11 12 syl GTopGrp0˙X
14 4 conncompid JTopOnX0˙X0˙S
15 10 13 14 syl2anc GTopGrp0˙S
16 15 ne0d GTopGrpS
17 df-ima zXy-GzS=ranzXy-GzS
18 resmpt SXzXy-GzS=zSy-Gz
19 8 18 ax-mp zXy-GzS=zSy-Gz
20 19 rneqi ranzXy-GzS=ranzSy-Gz
21 17 20 eqtri zXy-GzS=ranzSy-Gz
22 imassrn zXy-GzSranzXy-Gz
23 11 adantr GTopGrpySGGrp
24 23 adantr GTopGrpySzXGGrp
25 9 sselda GTopGrpySyX
26 25 adantr GTopGrpySzXyX
27 simpr GTopGrpySzXzX
28 eqid -G=-G
29 1 28 grpsubcl GGrpyXzXy-GzX
30 24 26 27 29 syl3anc GTopGrpySzXy-GzX
31 30 fmpttd GTopGrpySzXy-Gz:XX
32 31 frnd GTopGrpySranzXy-GzX
33 22 32 sstrid GTopGrpySzXy-GzSX
34 1 2 28 grpsubid GGrpyXy-Gy=0˙
35 23 25 34 syl2anc GTopGrpySy-Gy=0˙
36 simpr GTopGrpySyS
37 ovex y-GyV
38 eqid zSy-Gz=zSy-Gz
39 oveq2 z=yy-Gz=y-Gy
40 38 39 elrnmpt1s ySy-GyVy-GyranzSy-Gz
41 36 37 40 sylancl GTopGrpySy-GyranzSy-Gz
42 35 41 eqeltrrd GTopGrpyS0˙ranzSy-Gz
43 42 21 eleqtrrdi GTopGrpyS0˙zXy-GzS
44 eqid J=J
45 eqid +G=+G
46 eqid invgG=invgG
47 1 45 46 28 grpsubval yXzXy-Gz=y+GinvgGz
48 25 47 sylan GTopGrpySzXy-Gz=y+GinvgGz
49 48 mpteq2dva GTopGrpySzXy-Gz=zXy+GinvgGz
50 1 46 grpinvcl GGrpzXinvgGzX
51 23 50 sylan GTopGrpySzXinvgGzX
52 1 46 grpinvf GGrpinvgG:XX
53 11 52 syl GTopGrpinvgG:XX
54 53 adantr GTopGrpySinvgG:XX
55 54 feqmptd GTopGrpySinvgG=zXinvgGz
56 eqidd GTopGrpySwXy+Gw=wXy+Gw
57 oveq2 w=invgGzy+Gw=y+GinvgGz
58 51 55 56 57 fmptco GTopGrpySwXy+GwinvgG=zXy+GinvgGz
59 49 58 eqtr4d GTopGrpySzXy-Gz=wXy+GwinvgG
60 3 46 grpinvhmeo GTopGrpinvgGJHomeoJ
61 60 adantr GTopGrpySinvgGJHomeoJ
62 eqid wXy+Gw=wXy+Gw
63 62 1 45 3 tgplacthmeo GTopGrpyXwXy+GwJHomeoJ
64 25 63 syldan GTopGrpySwXy+GwJHomeoJ
65 hmeoco invgGJHomeoJwXy+GwJHomeoJwXy+GwinvgGJHomeoJ
66 61 64 65 syl2anc GTopGrpySwXy+GwinvgGJHomeoJ
67 59 66 eqeltrd GTopGrpySzXy-GzJHomeoJ
68 hmeocn zXy-GzJHomeoJzXy-GzJCnJ
69 67 68 syl GTopGrpySzXy-GzJCnJ
70 toponuni JTopOnXX=J
71 10 70 syl GTopGrpX=J
72 71 adantr GTopGrpySX=J
73 8 72 sseqtrid GTopGrpySSJ
74 4 conncompconn JTopOnX0˙XJ𝑡SConn
75 10 13 74 syl2anc GTopGrpJ𝑡SConn
76 75 adantr GTopGrpySJ𝑡SConn
77 44 69 73 76 connima GTopGrpySJ𝑡zXy-GzSConn
78 4 conncompss zXy-GzSX0˙zXy-GzSJ𝑡zXy-GzSConnzXy-GzSS
79 33 43 77 78 syl3anc GTopGrpySzXy-GzSS
80 21 79 eqsstrrid GTopGrpySranzSy-GzS
81 ovex y-GzV
82 81 38 fnmpti zSy-GzFnS
83 df-f zSy-Gz:SSzSy-GzFnSranzSy-GzS
84 82 83 mpbiran zSy-Gz:SSranzSy-GzS
85 80 84 sylibr GTopGrpySzSy-Gz:SS
86 38 fmpt zSy-GzSzSy-Gz:SS
87 85 86 sylibr GTopGrpySzSy-GzS
88 87 ralrimiva GTopGrpySzSy-GzS
89 1 28 issubg4 GGrpSSubGrpGSXSySzSy-GzS
90 11 89 syl GTopGrpSSubGrpGSXSySzSy-GzS
91 9 16 88 90 mpbir3and GTopGrpSSubGrpG
92 11 adantr GTopGrpyXzXy+GzSGGrp
93 eqid opp𝑔G=opp𝑔G
94 93 46 oppginv GGrpinvgG=invgopp𝑔G
95 92 94 syl GTopGrpyXzXy+GzSinvgG=invgopp𝑔G
96 95 fveq1d GTopGrpyXzXy+GzSinvgGinvgGy=invgopp𝑔GinvgGy
97 simprll GTopGrpyXzXy+GzSyX
98 1 46 grpinvinv GGrpyXinvgGinvgGy=y
99 92 97 98 syl2anc GTopGrpyXzXy+GzSinvgGinvgGy=y
100 96 99 eqtr3d GTopGrpyXzXy+GzSinvgopp𝑔GinvgGy=y
101 100 oveq1d GTopGrpyXzXy+GzSinvgopp𝑔GinvgGy+opp𝑔Gz=y+opp𝑔Gz
102 eqid +opp𝑔G=+opp𝑔G
103 45 93 102 oppgplus y+opp𝑔Gz=z+Gy
104 101 103 eqtrdi GTopGrpyXzXy+GzSinvgopp𝑔GinvgGy+opp𝑔Gz=z+Gy
105 1 46 grpinvcl GGrpyXinvgGyX
106 92 97 105 syl2anc GTopGrpyXzXy+GzSinvgGyX
107 simprlr GTopGrpyXzXy+GzSzX
108 99 oveq1d GTopGrpyXzXy+GzSinvgGinvgGy+Gz=y+Gz
109 simprr GTopGrpyXzXy+GzSy+GzS
110 108 109 eqeltrd GTopGrpyXzXy+GzSinvgGinvgGy+GzS
111 eqid G~QGS=G~QGS
112 1 46 45 111 eqgval GGrpSXinvgGyG~QGSzinvgGyXzXinvgGinvgGy+GzS
113 92 8 112 sylancl GTopGrpyXzXy+GzSinvgGyG~QGSzinvgGyXzXinvgGinvgGy+GzS
114 106 107 110 113 mpbir3and GTopGrpyXzXy+GzSinvgGyG~QGSz
115 1 2 3 4 111 tgpconncompeqg GTopGrpinvgGyXinvgGyG~QGS=x𝒫X|invgGyxJ𝑡xConn
116 106 115 syldan GTopGrpyXzXy+GzSinvgGyG~QGS=x𝒫X|invgGyxJ𝑡xConn
117 93 oppgtgp GTopGrpopp𝑔GTopGrp
118 117 adantr GTopGrpyXzXy+GzSopp𝑔GTopGrp
119 93 1 oppgbas X=Baseopp𝑔G
120 93 2 oppgid 0˙=0opp𝑔G
121 93 3 oppgtopn J=TopOpenopp𝑔G
122 eqid opp𝑔G~QGS=opp𝑔G~QGS
123 119 120 121 4 122 tgpconncompeqg opp𝑔GTopGrpinvgGyXinvgGyopp𝑔G~QGS=x𝒫X|invgGyxJ𝑡xConn
124 118 106 123 syl2anc GTopGrpyXzXy+GzSinvgGyopp𝑔G~QGS=x𝒫X|invgGyxJ𝑡xConn
125 116 124 eqtr4d GTopGrpyXzXy+GzSinvgGyG~QGS=invgGyopp𝑔G~QGS
126 125 eleq2d GTopGrpyXzXy+GzSzinvgGyG~QGSzinvgGyopp𝑔G~QGS
127 vex zV
128 fvex invgGyV
129 127 128 elec zinvgGyG~QGSinvgGyG~QGSz
130 127 128 elec zinvgGyopp𝑔G~QGSinvgGyopp𝑔G~QGSz
131 126 129 130 3bitr3g GTopGrpyXzXy+GzSinvgGyG~QGSzinvgGyopp𝑔G~QGSz
132 114 131 mpbid GTopGrpyXzXy+GzSinvgGyopp𝑔G~QGSz
133 eqid invgopp𝑔G=invgopp𝑔G
134 119 133 102 122 eqgval opp𝑔GTopGrpSXinvgGyopp𝑔G~QGSzinvgGyXzXinvgopp𝑔GinvgGy+opp𝑔GzS
135 118 8 134 sylancl GTopGrpyXzXy+GzSinvgGyopp𝑔G~QGSzinvgGyXzXinvgopp𝑔GinvgGy+opp𝑔GzS
136 132 135 mpbid GTopGrpyXzXy+GzSinvgGyXzXinvgopp𝑔GinvgGy+opp𝑔GzS
137 136 simp3d GTopGrpyXzXy+GzSinvgopp𝑔GinvgGy+opp𝑔GzS
138 104 137 eqeltrrd GTopGrpyXzXy+GzSz+GyS
139 138 expr GTopGrpyXzXy+GzSz+GyS
140 139 ralrimivva GTopGrpyXzXy+GzSz+GyS
141 1 45 isnsg2 SNrmSGrpGSSubGrpGyXzXy+GzSz+GyS
142 91 140 141 sylanbrc GTopGrpSNrmSGrpG