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

Theorem gsumval3 17619
 Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.)
Hypotheses
Ref Expression
gsumval3.b
gsumval3.0
gsumval3.p
gsumval3.z Cntz
gsumval3.g
gsumval3.a
gsumval3.f
gsumval3.c
gsumval3.m
gsumval3.h
gsumval3.n supp
gsumval3.w supp
Assertion
Ref Expression
gsumval3 g

Proof of Theorem gsumval3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumval3.g . . . . 5
2 gsumval3.a . . . . 5
3 gsumval3.0 . . . . . 6
43gsumz 16699 . . . . 5 g
51, 2, 4syl2anc 673 . . . 4 g
65adantr 472 . . 3 g
7 gsumval3.f . . . . . . 7
87feqmptd 5932 . . . . . 6
98adantr 472 . . . . 5
10 gsumval3.h . . . . . . . . . . . . . 14
11 f1f 5792 . . . . . . . . . . . . . 14
1210, 11syl 17 . . . . . . . . . . . . 13
1312ad2antrr 740 . . . . . . . . . . . 12
14 f1f1orn 5839 . . . . . . . . . . . . . . . 16
1510, 14syl 17 . . . . . . . . . . . . . . 15
1615adantr 472 . . . . . . . . . . . . . 14
17 f1ocnv 5840 . . . . . . . . . . . . . 14
18 f1of 5828 . . . . . . . . . . . . . 14
1916, 17, 183syl 18 . . . . . . . . . . . . 13
2019ffvelrnda 6037 . . . . . . . . . . . 12
21 fvco3 5957 . . . . . . . . . . . 12
2213, 20, 21syl2anc 673 . . . . . . . . . . 11
23 simpr 468 . . . . . . . . . . . . . . . 16
2423difeq2d 3540 . . . . . . . . . . . . . . 15
25 dif0 3749 . . . . . . . . . . . . . . 15
2624, 25syl6eq 2521 . . . . . . . . . . . . . 14
2726adantr 472 . . . . . . . . . . . . 13
2820, 27eleqtrrd 2552 . . . . . . . . . . . 12
29 fco 5751 . . . . . . . . . . . . . . 15
307, 12, 29syl2anc 673 . . . . . . . . . . . . . 14
3130adantr 472 . . . . . . . . . . . . 13
32 gsumval3.w . . . . . . . . . . . . . . 15 supp
3332eqimss2i 3473 . . . . . . . . . . . . . 14 supp
3433a1i 11 . . . . . . . . . . . . 13 supp
35 ovex 6336 . . . . . . . . . . . . . 14
3635a1i 11 . . . . . . . . . . . . 13
37 fvex 5889 . . . . . . . . . . . . . . 15
383, 37eqeltri 2545 . . . . . . . . . . . . . 14
3938a1i 11 . . . . . . . . . . . . 13
4031, 34, 36, 39suppssr 6965 . . . . . . . . . . . 12
4128, 40syldan 478 . . . . . . . . . . 11
42 f1ocnvfv2 6194 . . . . . . . . . . . . 13
4316, 42sylan 479 . . . . . . . . . . . 12
4443fveq2d 5883 . . . . . . . . . . 11
4522, 41, 443eqtr3rd 2514 . . . . . . . . . 10
46 fvex 5889 . . . . . . . . . . 11
4746elsnc 3984 . . . . . . . . . 10
4845, 47sylibr 217 . . . . . . . . 9
4948adantlr 729 . . . . . . . 8
50 eldif 3400 . . . . . . . . . . 11
51 gsumval3.n . . . . . . . . . . . . 13 supp
5238a1i 11 . . . . . . . . . . . . 13
537, 51, 2, 52suppssr 6965 . . . . . . . . . . . 12
5453, 47sylibr 217 . . . . . . . . . . 11
5550, 54sylan2br 484 . . . . . . . . . 10
5655adantlr 729 . . . . . . . . 9
5756anassrs 660 . . . . . . . 8
5849, 57pm2.61dan 808 . . . . . . 7
5958, 47sylib 201 . . . . . 6
6059mpteq2dva 4482 . . . . 5
619, 60eqtrd 2505 . . . 4
6261oveq2d 6324 . . 3 g g
63 gsumval3.b . . . . . . . 8
6463, 3mndidcl 16632 . . . . . . 7
651, 64syl 17 . . . . . 6
66 gsumval3.p . . . . . . 7
6763, 66, 3mndlid 16635 . . . . . 6
681, 65, 67syl2anc 673 . . . . 5
6968adantr 472 . . . 4
70 gsumval3.m . . . . . 6
71 nnuz 11218 . . . . . 6
7270, 71syl6eleq 2559 . . . . 5
7372adantr 472 . . . 4
7426eleq2d 2534 . . . . . 6
7574biimpar 493 . . . . 5
7631, 34, 36, 39suppssr 6965 . . . . 5
7775, 76syldan 478 . . . 4
7869, 73, 77seqid3 12295 . . 3
796, 62, 783eqtr4d 2515 . 2 g
80 fzf 11814 . . . . 5
81 ffn 5739 . . . . 5
82 ovelrn 6464 . . . . 5
8380, 81, 82mp2b 10 . . . 4
841ad2antrr 740 . . . . . . . . 9
85 simpr 468 . . . . . . . . . . 11
86 frel 5744 . . . . . . . . . . . . . . . . 17
87 reldm0 5058 . . . . . . . . . . . . . . . . 17
887, 86, 873syl 18 . . . . . . . . . . . . . . . 16
89 fdm 5745 . . . . . . . . . . . . . . . . . 18
907, 89syl 17 . . . . . . . . . . . . . . . . 17
9190eqeq1d 2473 . . . . . . . . . . . . . . . 16
9288, 91bitrd 261 . . . . . . . . . . . . . . 15
93 coeq1 4997 . . . . . . . . . . . . . . . . . . 19
94 co01 5357 . . . . . . . . . . . . . . . . . . 19
9593, 94syl6eq 2521 . . . . . . . . . . . . . . . . . 18
9695oveq1d 6323 . . . . . . . . . . . . . . . . 17 supp supp
97 supp0 6938 . . . . . . . . . . . . . . . . . 18 supp
9838, 97ax-mp 5 . . . . . . . . . . . . . . . . 17 supp
9996, 98syl6eq 2521 . . . . . . . . . . . . . . . 16 supp
10032, 99syl5eq 2517 . . . . . . . . . . . . . . 15
10192, 100syl6bir 237 . . . . . . . . . . . . . 14
102101necon3d 2664 . . . . . . . . . . . . 13
103102imp 436 . . . . . . . . . . . 12
104103adantr 472 . . . . . . . . . . 11
10585, 104eqnetrrd 2711 . . . . . . . . . 10
106 fzn0 11839 . . . . . . . . . 10
107105, 106sylib 201 . . . . . . . . 9
1087ad2antrr 740 . . . . . . . . . 10
10985feq2d 5725 . . . . . . . . . 10
110108, 109mpbid 215 . . . . . . . . 9
11163, 66, 84, 107, 110gsumval2 16601 . . . . . . . 8 g
112 frn 5747 . . . . . . . . . . . . . . 15
11310, 11, 1123syl 18 . . . . . . . . . . . . . 14
114113ad2antrr 740 . . . . . . . . . . . . 13
115114, 85sseqtrd 3454 . . . . . . . . . . . 12
116 fzssuz 11865 . . . . . . . . . . . . 13
117 uzssz 11202 . . . . . . . . . . . . . 14
118 zssre 10968 . . . . . . . . . . . . . 14
119117, 118sstri 3427 . . . . . . . . . . . . 13
120116, 119sstri 3427 . . . . . . . . . . . 12
121115, 120syl6ss 3430 . . . . . . . . . . 11
122 ltso 9732 . . . . . . . . . . 11
123 soss 4778 . . . . . . . . . . 11
124121, 122, 123mpisyl 21 . . . . . . . . . 10
125 fzfi 12223 . . . . . . . . . . . 12
126125a1i 11 . . . . . . . . . . . . . . 15
127 fex2 6767 . . . . . . . . . . . . . . 15
12812, 126, 2, 127syl3anc 1292 . . . . . . . . . . . . . 14
129 f1oen3g 7603 . . . . . . . . . . . . . 14
130128, 15, 129syl2anc 673 . . . . . . . . . . . . 13
131 enfi 7806 . . . . . . . . . . . . 13
132130, 131syl 17 . . . . . . . . . . . 12
133125, 132mpbii 216 . . . . . . . . . . 11
134133ad2antrr 740 . . . . . . . . . 10
135 fz1iso 12666 . . . . . . . . . 10
136124, 134, 135syl2anc 673 . . . . . . . . 9
13770nnnn0d 10949 . . . . . . . . . . . . . . . 16
138 hashfz1 12567 . . . . . . . . . . . . . . . 16
139137, 138syl 17 . . . . . . . . . . . . . . 15
140 hashen 12568 . . . . . . . . . . . . . . . . 17
141125, 133, 140sylancr 676 . . . . . . . . . . . . . . . 16
142130, 141mpbird 240 . . . . . . . . . . . . . . 15
143139, 142eqtr3d 2507 . . . . . . . . . . . . . 14
144143ad2antrr 740 . . . . . . . . . . . . 13
145144fveq2d 5883 . . . . . . . . . . . 12
1461ad2antrr 740 . . . . . . . . . . . . . 14
14763, 66mndcl 16623 . . . . . . . . . . . . . . 15
1481473expb 1232 . . . . . . . . . . . . . 14
149146, 148sylan 479 . . . . . . . . . . . . 13
150 gsumval3.c . . . . . . . . . . . . . . . . 17
151150ad2antrr 740 . . . . . . . . . . . . . . . 16
152151sselda 3418 . . . . . . . . . . . . . . 15
153 gsumval3.z . . . . . . . . . . . . . . . 16 Cntz
15466, 153cntzi 17061 . . . . . . . . . . . . . . 15
155152, 154sylan 479 . . . . . . . . . . . . . 14
156155anasss 659 . . . . . . . . . . . . 13
15763, 66mndass 16624 . . . . . . . . . . . . . 14
158146, 157sylan 479 . . . . . . . . . . . . 13
15972ad2antrr 740 . . . . . . . . . . . . 13
1607ad2antrr 740 . . . . . . . . . . . . . 14
161 frn 5747 . . . . . . . . . . . . . 14
162160, 161syl 17 . . . . . . . . . . . . 13
163 simprr 774 . . . . . . . . . . . . . . . . 17
164 isof1o 6234 . . . . . . . . . . . . . . . . 17
165163, 164syl 17 . . . . . . . . . . . . . . . 16
166144oveq2d 6324 . . . . . . . . . . . . . . . . 17
167 f1oeq2 5819 . . . . . . . . . . . . . . . . 17
168166, 167syl 17 . . . . . . . . . . . . . . . 16
169165, 168mpbird 240 . . . . . . . . . . . . . . 15
170 f1ocnv 5840 . . . . . . . . . . . . . . 15
171169, 170syl 17 . . . . . . . . . . . . . 14
17215ad2antrr 740 . . . . . . . . . . . . . 14
173 f1oco 5850 . . . . . . . . . . . . . 14
174171, 172, 173syl2anc 673 . . . . . . . . . . . . 13
175 ffn 5739 . . . . . . . . . . . . . . . . 17
176 dffn4 5812 . . . . . . . . . . . . . . . . 17
177175, 176sylib 201 . . . . . . . . . . . . . . . 16
178 fof 5806 . . . . . . . . . . . . . . . 16
179160, 177, 1783syl 18 . . . . . . . . . . . . . . 15
180 f1of 5828 . . . . . . . . . . . . . . . . 17
181169, 180syl 17 . . . . . . . . . . . . . . . 16
182113ad2antrr 740 . . . . . . . . . . . . . . . 16
183181, 182fssd 5750 . . . . . . . . . . . . . . 15
184 fco 5751 . . . . . . . . . . . . . . 15
185179, 183, 184syl2anc 673 . . . . . . . . . . . . . 14
186185ffvelrnda 6037 . . . . . . . . . . . . 13
187 f1ococnv2 5854 . . . . . . . . . . . . . . . . . . . . . 22
188169, 187syl 17 . . . . . . . . . . . . . . . . . . . . 21
189188coeq1d 5001 . . . . . . . . . . . . . . . . . . . 20
190 f1of 5828 . . . . . . . . . . . . . . . . . . . . 21
191 fcoi2 5770 . . . . . . . . . . . . . . . . . . . . 21
192172, 190, 1913syl 18 . . . . . . . . . . . . . . . . . . . 20
193189, 192eqtr2d 2506 . . . . . . . . . . . . . . . . . . 19
194 coass 5361 . . . . . . . . . . . . . . . . . . 19
195193, 194syl6eq 2521 . . . . . . . . . . . . . . . . . 18
196195coeq2d 5002 . . . . . . . . . . . . . . . . 17
197 coass 5361 . . . . . . . . . . . . . . . . 17
198196, 197syl6eqr 2523 . . . . . . . . . . . . . . . 16
199198fveq1d 5881 . . . . . . . . . . . . . . 15
200199adantr 472 . . . . . . . . . . . . . 14
201 f1of 5828 . . . . . . . . . . . . . . . . 17
202169, 170, 2013syl 18 . . . . . . . . . . . . . . . 16
203172, 190syl 17 . . . . . . . . . . . . . . . 16
204 fco 5751 . . . . . . . . . . . . . . . 16
205202, 203, 204syl2anc 673 . . . . . . . . . . . . . . 15
206 fvco3 5957 . . . . . . . . . . . . . . 15
207205, 206sylan 479 . . . . . . . . . . . . . 14
208200, 207eqtrd 2505 . . . . . . . . . . . . 13
209149, 156, 158, 159, 162, 174, 186, 208seqf1o 12292 . . . . . . . . . . . 12
21063, 66, 3mndlid 16635 . . . . . . . . . . . . . 14
211146, 210sylan 479 . . . . . . . . . . . . 13
21263, 66, 3mndrid 16636 . . . . . . . . . . . . . 14
213146, 212sylan 479 . . . . . . . . . . . . 13
214146, 64syl 17 . . . . . . . . . . . . 13
215 fdm 5745 . . . . . . . . . . . . . . . . 17
21610, 11, 2153syl 18 . . . . . . . . . . . . . . . 16
217 eluzfz1 11832 . . . . . . . . . . . . . . . . 17
218 ne0i 3728 . . . . . . . . . . . . . . . . 17
21972, 217, 2183syl 18 . . . . . . . . . . . . . . . 16
220216, 219eqnetrd 2710 . . . . . . . . . . . . . . 15
221 dm0rn0 5057 . . . . . . . . . . . . . . . 16
222221necon3bii 2695 . . . . . . . . . . . . . . 15
223220, 222sylib 201 . . . . . . . . . . . . . 14
224223ad2antrr 740 . . . . . . . . . . . . 13
225115adantrr 731 . . . . . . . . . . . . 13
226 simprl 772 . . . . . . . . . . . . . . . 16
227226eleq2d 2534 . . . . . . . . . . . . . . 15
228227biimpar 493 . . . . . . . . . . . . . 14
229160ffvelrnda 6037 . . . . . . . . . . . . . 14
230228, 229syldan 478 . . . . . . . . . . . . 13
231226difeq1d 3539 . . . . . . . . . . . . . . . 16
232231eleq2d 2534 . . . . . . . . . . . . . . 15
233232biimpar 493 . . . . . . . . . . . . . 14
234 simpll 768 . . . . . . . . . . . . . . 15
235234, 53sylan 479 . . . . . . . . . . . . . 14
236233, 235syldan 478 . . . . . . . . . . . . 13
237 f1of 5828 . . . . . . . . . . . . . . 15
238163, 164, 2373syl 18 . . . . . . . . . . . . . 14
239 fvco3 5957 . . . . . . . . . . . . . 14
240238, 239sylan 479 . . . . . . . . . . . . 13
241211, 213, 149, 214, 163, 224, 225, 230, 236, 240seqcoll2 12669 . . . . . . . . . . . 12
242145, 209, 2413eqtr4d 2515 . . . . . . . . . . 11
243242expr 626 . . . . . . . . . 10
244243exlimdv 1787 . . . . . . . . 9
245136, 244mpd 15 . . . . . . . 8
246111, 245eqtr4d 2508 . . . . . . 7 g
247246ex 441 . . . . . 6 g
248247rexlimdvw 2874 . . . . 5 g
249248rexlimdvw 2874 . . . 4 g
25083, 249syl5bi 225 . . 3 g
251 suppssdm 6946 . . . . . . . . . . 11 supp
25232, 251eqsstri 3448 . . . . . . . . . 10
253 fdm 5745 . . . . . . . . . . 11
25430, 253syl 17 . . . . . . . . . 10
255252, 254syl5sseq 3466 . . . . . . . . 9
256 fzssuz 11865 . . . . . . . . . . 11
257256, 71sseqtr4i 3451 . . . . . . . . . 10
258 nnssre 10635 . . . . . . . . . 10
259257, 258sstri 3427 . . . . . . . . 9
260255, 259syl6ss 3430 . . . . . . . 8
261 soss 4778 . . . . . . . 8
262260, 122, 261mpisyl 21 . . . . . . 7
263 ssfi 7810 . . . . . . . 8
264125, 255, 263sylancr 676 . . . . . . 7
265 fz1iso 12666 . . . . . . 7
266262, 264, 265syl2anc 673 . . . . . 6
267266ad2antrr 740 . . . . 5
26863, 3, 66, 153, 1, 2, 7, 150, 70, 10, 51, 32gsumval3lem2 17618 . . . . . . . 8 g
2691ad2antrr 740 . . . . . . . . . 10
270269, 210sylan 479 . . . . . . . . 9
271269, 212sylan 479 . . . . . . . . 9
272269, 148sylan 479 . . . . . . . . 9
273269, 64syl 17 . . . . . . . . 9
274 simprr 774 . . . . . . . . 9
275 simplr 770 . . . . . . . . 9
276255ad2antrr 740 . . . . . . . . 9
27730ad2antrr 740 . . . . . . . . . 10
278277ffvelrnda 6037 . . . . . . . . 9
27933a1i 11 . . . . . . . . . 10 supp
28035a1i 11 . . . . . . . . . 10
28138a1i 11 . . . . . . . . . 10
282277, 279, 280, 281suppssr 6965 . . . . . . . . 9
283 coass 5361 . . . . . . . . . . 11
284283fveq1i 5880 . . . . . . . . . 10
285 isof1o 6234 . . . . . . . . . . . 12
286 f1of 5828 . . . . . . . . . . . 12
287274, 285, 2863syl 18 . . . . . . . . . . 11
288 fvco3 5957 . . . . . . . . . . 11
289287, 288sylan 479 . . . . . . . . . 10
290284, 289syl5eqr 2519 . . . . . . . . 9
291270, 271, 272, 273, 274, 275, 276, 278, 282, 290seqcoll2 12669 . . . . . . . 8
292268, 291eqtr4d 2508 . . . . . . 7 g
293292expr 626 . . . . . 6 g
294293exlimdv 1787 . . . . 5 g
295267, 294mpd 15 . . . 4 g
296295ex 441 . . 3 g
297250, 296pm2.61d 163 . 2 g
29879, 297pm2.61dane 2730 1 g
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904   wne 2641  wrex 2757  cvv 3031   cdif 3387   wss 3390  c0 3722  cpw 3942  csn 3959   class class class wbr 4395   cmpt 4454   cid 4749   wor 4759   cxp 4837  ccnv 4838   cdm 4839   crn 4840   cres 4841   ccom 4843   wrel 4844   wfn 5584  wf 5585  wf1 5586  wfo 5587  wf1o 5588  cfv 5589   wiso 5590  (class class class)co 6308   supp csupp 6933   cen 7584  cfn 7587  cr 9556  c1 9558   clt 9693  cn 10631  cn0 10893  cz 10961  cuz 11182  cfz 11810   cseq 12251  chash 12553  cbs 15199   cplusg 15268  c0g 15416   g cgsu 15417  cmnd 16613  Cntzccntz 17047 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-oi 8043  df-card 8391  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-fzo 11943  df-seq 12252  df-hash 12554  df-0g 15418  df-gsum 15419  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-cntz 17049 This theorem is referenced by:  gsumzres  17621  gsumzcl2  17622  gsumzf1o  17624  gsumzaddlem  17632  gsumconst  17645  gsumzmhm  17648  gsumzoppg  17655  gsumfsum  19111  wilthlem3  24074
 Copyright terms: Public domain W3C validator