Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  divstgplem Structured version   Unicode version

Theorem divstgplem 18150
 Description: Lemma for divstgp 18151. (Contributed by Mario Carneiro, 18-Sep-2015.)
Hypotheses
Ref Expression
divstgp.h s ~QG
divstgpopn.x
divstgpopn.j
divstgpopn.k
divstgpopn.f ~QG
divstgplem.m ~QG
Assertion
Ref Expression
divstgplem NrmSGrp
Distinct variable groups:   ,,,   ,,,   ,,   ,,,   ,,,   ,,,   ,,,
Allowed substitution hints:   ()   (,,)

Proof of Theorem divstgplem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 divstgp.h . . . 4 s ~QG
21divsgrp 14995 . . 3 NrmSGrp
41a1i 11 . . . . . . 7 NrmSGrp s ~QG
5 divstgpopn.x . . . . . . . 8
65a1i 11 . . . . . . 7 NrmSGrp
7 divstgpopn.f . . . . . . 7 ~QG
8 ovex 6106 . . . . . . . 8 ~QG
98a1i 11 . . . . . . 7 NrmSGrp ~QG
10 simpl 444 . . . . . . 7 NrmSGrp
114, 6, 7, 9, 10divsval 13767 . . . . . 6 NrmSGrp s
124, 6, 7, 9, 10divslem 13768 . . . . . 6 NrmSGrp ~QG
13 divstgpopn.j . . . . . 6
14 divstgpopn.k . . . . . 6
1511, 6, 12, 10, 13, 14imastopn 17752 . . . . 5 NrmSGrp qTop
1613, 5tgptopon 18112 . . . . . . 7 TopOn
1716adantr 452 . . . . . 6 NrmSGrp TopOn
18 qtoptopon 17736 . . . . . 6 TopOn ~QG qTop TopOn ~QG
1917, 12, 18syl2anc 643 . . . . 5 NrmSGrp qTop TopOn ~QG
2015, 19eqeltrd 2510 . . . 4 NrmSGrp TopOn ~QG
214, 6, 9, 10divsbas 13770 . . . . 5 NrmSGrp ~QG
2221fveq2d 5732 . . . 4 NrmSGrp TopOn ~QG TopOn
2320, 22eleqtrd 2512 . . 3 NrmSGrp TopOn
24 eqid 2436 . . . 4
2524, 14istps 17001 . . 3 TopOn
2623, 25sylibr 204 . 2 NrmSGrp
27 eqid 2436 . . . . 5
2824, 27grpsubf 14868 . . . 4
293, 28syl 16 . . 3 NrmSGrp
30 cnvimass 5224 . . . . . . . . 9
31 fdm 5595 . . . . . . . . . . 11
3229, 31syl 16 . . . . . . . . . 10 NrmSGrp
3332adantr 452 . . . . . . . . 9 NrmSGrp
3430, 33syl5sseq 3396 . . . . . . . 8 NrmSGrp
35 relxp 4983 . . . . . . . 8
36 relss 4963 . . . . . . . 8
3734, 35, 36ee10 1385 . . . . . . 7 NrmSGrp
3834sseld 3347 . . . . . . . 8 NrmSGrp
39 vex 2959 . . . . . . . . . . . . . 14
4039elqs 6957 . . . . . . . . . . . . 13 ~QG ~QG
4121adantr 452 . . . . . . . . . . . . . 14 NrmSGrp ~QG
4241eleq2d 2503 . . . . . . . . . . . . 13 NrmSGrp ~QG
4340, 42syl5bbr 251 . . . . . . . . . . . 12 NrmSGrp ~QG
44 vex 2959 . . . . . . . . . . . . . 14
4544elqs 6957 . . . . . . . . . . . . 13 ~QG ~QG
4641eleq2d 2503 . . . . . . . . . . . . 13 NrmSGrp ~QG
4745, 46syl5bbr 251 . . . . . . . . . . . 12 NrmSGrp ~QG
4843, 47anbi12d 692 . . . . . . . . . . 11 NrmSGrp ~QG ~QG
49 reeanv 2875 . . . . . . . . . . 11 ~QG ~QG ~QG ~QG
50 opelxp 4908 . . . . . . . . . . 11
5148, 49, 503bitr4g 280 . . . . . . . . . 10 NrmSGrp ~QG ~QG
523ad2antrr 707 . . . . . . . . . . . . . . 15 NrmSGrp
5352, 28syl 16 . . . . . . . . . . . . . 14 NrmSGrp
54 ffn 5591 . . . . . . . . . . . . . 14
55 elpreima 5850 . . . . . . . . . . . . . 14 ~QG ~QG ~QG ~QG ~QG ~QG
5653, 54, 553syl 19 . . . . . . . . . . . . 13 NrmSGrp ~QG ~QG ~QG ~QG ~QG ~QG
57 df-ov 6084 . . . . . . . . . . . . . . . . 17 ~QG ~QG ~QG ~QG
58 simpllr 736 . . . . . . . . . . . . . . . . . 18 NrmSGrp NrmSGrp
59 simprl 733 . . . . . . . . . . . . . . . . . 18 NrmSGrp
60 simprr 734 . . . . . . . . . . . . . . . . . 18 NrmSGrp
61 eqid 2436 . . . . . . . . . . . . . . . . . . 19
621, 5, 61, 27divssub 15000 . . . . . . . . . . . . . . . . . 18 NrmSGrp ~QG ~QG ~QG
6358, 59, 60, 62syl3anc 1184 . . . . . . . . . . . . . . . . 17 NrmSGrp ~QG ~QG ~QG
6457, 63syl5eqr 2482 . . . . . . . . . . . . . . . 16 NrmSGrp ~QG ~QG ~QG
6564eleq1d 2502 . . . . . . . . . . . . . . 15 NrmSGrp ~QG ~QG ~QG
66 simpr 448 . . . . . . . . . . . . . . . . 17 NrmSGrp
67 divstgplem.m . . . . . . . . . . . . . . . . . . . . . 22 ~QG
68 tgpgrp 18108 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6968adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NrmSGrp
705, 61grpsubf 14868 . . . . . . . . . . . . . . . . . . . . . . . . . 26
71 ffn 5591 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7269, 70, 713syl 19 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp
73 fnov 6178 . . . . . . . . . . . . . . . . . . . . . . . . 25
7472, 73sylib 189 . . . . . . . . . . . . . . . . . . . . . . . 24 NrmSGrp
7513, 61tgpsubcn 18120 . . . . . . . . . . . . . . . . . . . . . . . . 25
7675adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24 NrmSGrp
7774, 76eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . . . . 23 NrmSGrp
78 ecexg 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ~QG ~QG
798, 78ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ~QG
8079, 7fnmpti 5573 . . . . . . . . . . . . . . . . . . . . . . . . . 26
81 qtopid 17737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 TopOn qTop
8217, 80, 81sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp qTop
8315oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp qTop
8482, 83eleqtrrd 2513 . . . . . . . . . . . . . . . . . . . . . . . 24 NrmSGrp
857, 84syl5eqelr 2521 . . . . . . . . . . . . . . . . . . . . . . 23 NrmSGrp ~QG
86 eceq1 6941 . . . . . . . . . . . . . . . . . . . . . . 23 ~QG ~QG
8717, 17, 77, 17, 85, 86cnmpt21 17703 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp ~QG
8867, 87syl5eqel 2520 . . . . . . . . . . . . . . . . . . . . 21 NrmSGrp
8988ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
90 simplr 732 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
91 cnima 17329 . . . . . . . . . . . . . . . . . . . 20
9289, 90, 91syl2anc 643 . . . . . . . . . . . . . . . . . . 19 NrmSGrp
9317ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp TopOn
94 eltx 17600 . . . . . . . . . . . . . . . . . . . 20 TopOn TopOn
9593, 93, 94syl2anc 643 . . . . . . . . . . . . . . . . . . 19 NrmSGrp
9692, 95mpbid 202 . . . . . . . . . . . . . . . . . 18 NrmSGrp
97 ecexg 6909 . . . . . . . . . . . . . . . . . . . . . . 23 ~QG ~QG
988, 97ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22 ~QG
9967, 98fnmpt2i 6420 . . . . . . . . . . . . . . . . . . . . 21
100 elpreima 5850 . . . . . . . . . . . . . . . . . . . . 21
10199, 100ax-mp 8 . . . . . . . . . . . . . . . . . . . 20
102 opelxp 4908 . . . . . . . . . . . . . . . . . . . . 21
103102anbi1i 677 . . . . . . . . . . . . . . . . . . . 20
104 df-ov 6084 . . . . . . . . . . . . . . . . . . . . . . 23
105 oveq12 6090 . . . . . . . . . . . . . . . . . . . . . . . . 25
106 eceq1 6941 . . . . . . . . . . . . . . . . . . . . . . . . 25 ~QG ~QG
107105, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 ~QG ~QG
108 ecexg 6909 . . . . . . . . . . . . . . . . . . . . . . . . 25 ~QG ~QG
1098, 108ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24 ~QG
110107, 67, 109ovmpt2a 6204 . . . . . . . . . . . . . . . . . . . . . . 23 ~QG
111104, 110syl5eqr 2482 . . . . . . . . . . . . . . . . . . . . . 22 ~QG
112111eleq1d 2502 . . . . . . . . . . . . . . . . . . . . 21 ~QG
113112pm5.32i 619 . . . . . . . . . . . . . . . . . . . 20 ~QG
114101, 103, 1133bitri 263 . . . . . . . . . . . . . . . . . . 19 ~QG
115 eleq1 2496 . . . . . . . . . . . . . . . . . . . . . . 23
116 opelxp 4908 . . . . . . . . . . . . . . . . . . . . . . 23
117115, 116syl6bb 253 . . . . . . . . . . . . . . . . . . . . . 22
118117anbi1d 686 . . . . . . . . . . . . . . . . . . . . 21
1191182rexbidv 2748 . . . . . . . . . . . . . . . . . . . 20
120119rspccv 3049 . . . . . . . . . . . . . . . . . . 19
121114, 120syl5bir 210 . . . . . . . . . . . . . . . . . 18 ~QG
12296, 121syl 16 . . . . . . . . . . . . . . . . 17 NrmSGrp ~QG
12366, 122mpand 657 . . . . . . . . . . . . . . . 16 NrmSGrp ~QG
124 simp-4l 743 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
12558adantr 452 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp NrmSGrp
126 simprll 739 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
1271, 5, 13, 14, 7divstgpopn 18149 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
128124, 125, 126, 127syl3anc 1184 . . . . . . . . . . . . . . . . . . 19 NrmSGrp
129 simprlr 740 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
1301, 5, 13, 14, 7divstgpopn 18149 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
131124, 125, 129, 130syl3anc 1184 . . . . . . . . . . . . . . . . . . 19 NrmSGrp
13259adantr 452 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp
133 eceq1 6941 . . . . . . . . . . . . . . . . . . . . . . 23 ~QG ~QG
134133, 7, 79fvmpt3i 5809 . . . . . . . . . . . . . . . . . . . . . 22 ~QG
135132, 134syl 16 . . . . . . . . . . . . . . . . . . . . 21 NrmSGrp ~QG
136124, 16syl 16 . . . . . . . . . . . . . . . . . . . . . . 23 NrmSGrp TopOn
137 toponss 16994 . . . . . . . . . . . . . . . . . . . . . . 23 TopOn
138136, 126, 137syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp
139 simprrl 741 . . . . . . . . . . . . . . . . . . . . . . 23 NrmSGrp
140139simpld 446 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp
141 fnfvima 5976 . . . . . . . . . . . . . . . . . . . . . . 23
14280, 141mp3an1 1266 . . . . . . . . . . . . . . . . . . . . . 22
143138, 140, 142syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21 NrmSGrp
144135, 143eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp ~QG
14560adantr 452 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp
146 eceq1 6941 . . . . . . . . . . . . . . . . . . . . . . 23 ~QG ~QG
147146, 7, 79fvmpt3i 5809 . . . . . . . . . . . . . . . . . . . . . 22 ~QG
148145, 147syl 16 . . . . . . . . . . . . . . . . . . . . 21 NrmSGrp ~QG
149 toponss 16994 . . . . . . . . . . . . . . . . . . . . . . 23 TopOn
150136, 129, 149syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp
151139simprd 450 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp
152 fnfvima 5976 . . . . . . . . . . . . . . . . . . . . . . 23
15380, 152mp3an1 1266 . . . . . . . . . . . . . . . . . . . . . 22
154150, 151, 153syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21 NrmSGrp
155148, 154eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp ~QG
156 opelxpi 4910 . . . . . . . . . . . . . . . . . . . 20 ~QG ~QG ~QG ~QG
157144, 155, 156syl2anc 643 . . . . . . . . . . . . . . . . . . 19 NrmSGrp ~QG ~QG
158138sselda 3348 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp
159150sselda 3348 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp
160158, 159anim12dan 811 . . . . . . . . . . . . . . . . . . . . . . . 24 NrmSGrp
161 eceq1 6941 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ~QG ~QG
162161, 7, 79fvmpt3i 5809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ~QG
163 eceq1 6941 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ~QG ~QG
164163, 7, 79fvmpt3i 5809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ~QG
165 opeq12 3986 . . . . . . . . . . . . . . . . . . . . . . . . 25 ~QG ~QG ~QG ~QG
166162, 164, 165syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . 24 ~QG ~QG
167160, 166syl 16 . . . . . . . . . . . . . . . . . . . . . . 23 NrmSGrp ~QG ~QG
168125adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NrmSGrp NrmSGrp
1691, 5, 24divseccl 14996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NrmSGrp ~QG
1701, 5, 24divseccl 14996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NrmSGrp ~QG
171169, 170anim12dan 811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NrmSGrp ~QG ~QG
172168, 160, 171syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp ~QG ~QG
173 opelxpi 4910 . . . . . . . . . . . . . . . . . . . . . . . . 25 ~QG ~QG ~QG ~QG
174172, 173syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 NrmSGrp ~QG ~QG
1751, 5, 61, 27divssub 15000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 NrmSGrp ~QG ~QG ~QG
1761753expb 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NrmSGrp ~QG ~QG ~QG
177168, 160, 176syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NrmSGrp ~QG ~QG ~QG
178 oveq12 6090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
179 eceq1 6941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ~QG ~QG
180178, 179syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ~QG ~QG
181 ecexg 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ~QG ~QG
1828, 181ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ~QG
183180, 67, 182ovmpt2a 6204 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ~QG
184160, 183syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NrmSGrp ~QG
185177, 184eqtr4d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NrmSGrp ~QG ~QG
186 df-ov 6084 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ~QG ~QG ~QG ~QG
187 df-ov 6084 . . . . . . . . . . . . . . . . . . . . . . . . . 26
188185, 186, 1873eqtr3g 2491 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp ~QG ~QG
189 opelxpi 4910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
190 simprrr 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NrmSGrp
191190sselda 3348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NrmSGrp
192189, 191sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NrmSGrp
193 elpreima 5850 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
19499, 193ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
195194simprbi 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26
196192, 195syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp
197188, 196eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . . 24 NrmSGrp ~QG ~QG
19853, 54syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NrmSGrp
199198ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25 NrmSGrp
200 elpreima 5850 . . . . . . . . . . . . . . . . . . . . . . . . 25 ~QG ~QG ~QG ~QG ~QG ~QG
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 NrmSGrp ~QG ~QG ~QG ~QG ~QG ~QG
202174, 197, 201mpbir2and 889 . . . . . . . . . . . . . . . . . . . . . . 23 NrmSGrp ~QG ~QG
203167, 202eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . 22 NrmSGrp
204203ralrimivva 2798 . . . . . . . . . . . . . . . . . . . . 21 NrmSGrp
205 opeq1 3984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
206205eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . 26
207206ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . . . 25
208207ralima 5978 . . . . . . . . . . . . . . . . . . . . . . . 24
20980, 208mpan 652 . . . . . . . . . . . . . . . . . . . . . . 23
210 opeq2 3985 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
211210eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . 26
212211ralima 5978 . . . . . . . . . . . . . . . . . . . . . . . . 25
21380, 212mpan 652 . . . . . . . . . . . . . . . . . . . . . . . 24
214213ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . 23
215209, 214sylan9bb 681 . . . . . . . . . . . . . . . . . . . . . 22
216138, 150, 215syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21 NrmSGrp
217204, 216mpbird 224 . . . . . . . . . . . . . . . . . . . 20 NrmSGrp
218 dfss3 3338 . . . . . . . . . . . . . . . . . . . . 21
219 eleq1 2496 . . . . . . . . . . . . . . . . . . . . . 22
220219ralxp 5016 . . . . . . . . . . . . . . . . . . . . 21
221218, 220bitri 241 . . . . . . . . . . . . . . . . . . . 20
222217, 221sylibr 204 . . . . . . . . . . . . . . . . . . 19 NrmSGrp
223 xpeq1 4892 . . . . . . . . . . . . . . . . . . . . . 22
224223eleq2d 2503 . . . . . . . . . . . . . . . . . . . . 21 ~QG ~QG ~QG ~QG
225223sseq1d 3375 . . . . . . . . . . . . . . . . . . . . 21
226224, 225anbi12d 692 . . . . . . . . . . . . . . . . . . . 20 ~QG ~QG ~QG ~QG
227 xpeq2 4893 . . . . . . . . . . . . . . . . . . . . . 22
228227eleq2d 2503 . . . . . . . . . . . . . . . . . . . . 21 ~QG ~QG ~QG ~QG
229227sseq1d 3375 . . . . . . . . . . . . . . . . . . . . 21
230228, 229anbi12d 692 . . . . . . . . . . . . . . . . . . . 20 ~QG ~QG ~QG ~QG
231226, 230rspc2ev 3060 . . . . . . . . . . . . . . . . . . 19 ~QG ~QG ~QG ~QG
232128, 131, 157, 222, 231syl112anc 1188 . . . . . . . . . . . . . . . . . 18 NrmSGrp ~QG ~QG
233232expr 599 . . . . . . . . . . . . . . . . 17 NrmSGrp ~QG ~QG
234233rexlimdvva 2837 . . . . . . . . . . . . . . . 16 NrmSGrp ~QG ~QG
235123, 234syld 42 . . . . . . . . . . . . . . 15 NrmSGrp ~QG ~QG ~QG
23665, 235sylbid 207 . . . . . . . . . . . . . 14 NrmSGrp ~QG ~QG ~QG ~QG
237236adantld 454 . . . . . . . . . . . . 13 NrmSGrp ~QG ~QG ~QG ~QG ~QG ~QG
23856, 237sylbid 207 . . . . . . . . . . . 12 NrmSGrp ~QG ~QG ~QG ~QG
239 opeq12 3986 . . . . . . . . . . . . . 14 ~QG ~QG ~QG ~QG
240239eleq1d 2502 . . . . . . . . . . . . 13 ~QG ~QG ~QG ~QG
241239eleq1d 2502 . . . . . . . . . . . . . 14 ~QG ~QG ~QG ~QG
242 opex 4427 . . . . . . . . . . . . . . 15 ~QG ~QG
243 eleq1 2496 . . . . . . . . . . . . . . . . 17 ~QG ~QG ~QG ~QG
244243anbi1d 686 . . . . . . . . . . . . . . . 16 ~QG ~QG ~QG ~QG
2452442rexbidv 2748 . . . . . . . . . . . . . . 15 ~QG ~QG ~QG ~QG
246242, 245elab 3082 . . . . . . . . . . . . . 14 ~QG ~QG ~QG ~QG
247241, 246syl6bb 253 . . . . . . . . . . . . 13 ~QG ~QG ~QG ~QG
248240, 247imbi12d 312 . . . . . . . . . . . 12 ~QG ~QG ~QG ~QG ~QG ~QG
249238, 248syl5ibrcom 214 . . . . . . . . . . 11 NrmSGrp ~QG ~QG
250249rexlimdvva 2837 . . . . . . . . . 10 NrmSGrp ~QG ~QG
25151, 250sylbird 227 . . . . . . . . 9 NrmSGrp
252251com23 74 . . . . . . . 8 NrmSGrp
25338, 252mpdd 38 . . . . . . 7 NrmSGrp
25437, 253relssdv 4968 . . . . . 6 NrmSGrp
255 ssabral 3414 . . . . . 6
256254, 255sylib 189 . . . . 5 NrmSGrp
257 eltx 17600 . . . . . . 7 TopOn TopOn
25823, 23, 257syl2anc 643 . . . . . 6 NrmSGrp
259258adantr 452 . . . . 5 NrmSGrp
260256, 259mpbird 224 . . . 4 NrmSGrp
261260ralrimiva 2789 . . 3 NrmSGrp
262 txtopon 17623 . . . . 5 TopOn TopOn TopOn
26323, 23, 262syl2anc 643 . . . 4 NrmSGrp TopOn
264 iscn 17299 . . . 4 TopOn TopOn
265263, 23, 264syl2anc 643 . . 3 NrmSGrp
26629, 261, 265mpbir2and 889 . 2 NrmSGrp
26714, 27istgp2 18121 . 2
2683, 26, 266, 267syl3anbrc 1138 1 NrmSGrp
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  cab 2422  wral 2705  wrex 2706  cvv 2956   wss 3320  cop 3817   cmpt 4266   cxp 4876  ccnv 4877   cdm 4878  cima 4881   wrel 4883   wfn 5449  wf 5450  wfo 5452  cfv 5454  (class class class)co 6081   cmpt2 6083  cec 6903  cqs 6904  cbs 13469  ctopn 13649   qTop cqtop 13729   s cqus 13731  cgrp 14685  csg 14688  NrmSGrpcnsg 14939   ~QG cqg 14940  TopOnctopon 16959  ctps 16961   ccn 17288   ctx 17592  ctgp 18101 This theorem is referenced by:  divstgp  18151 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-tpos 6479  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-oadd 6728  df-er 6905  df-ec 6907  df-qs 6911  df-map 7020  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-sup 7446  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-nn 10001  df-2 10058  df-3 10059  df-4 10060  df-5 10061  df-6 10062  df-7 10063  df-8 10064  df-9 10065  df-10 10066  df-n0 10222  df-z 10283  df-dec 10383  df-uz 10489  df-fz 11044  df-struct 13471  df-ndx 13472  df-slot 13473  df-base 13474  df-sets 13475  df-ress 13476  df-plusg 13542  df-mulr 13543  df-sca 13545  df-vsca 13546  df-tset 13548  df-ple 13549  df-ds 13551  df-rest 13650  df-topn 13651  df-topgen 13667  df-0g 13727  df-qtop 13733  df-imas 13734  df-divs 13735  df-mnd 14690  df-plusf 14691  df-grp 14812  df-minusg 14813  df-sbg 14814  df-subg 14941  df-nsg 14942  df-eqg 14943  df-oppg 15142  df-top 16963  df-bases 16965  df-topon 16966  df-topsp 16967  df-cn 17291  df-cnp 17292  df-tx 17594  df-hmeo 17787  df-tmd 18102  df-tgp 18103
 Copyright terms: Public domain W3C validator