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

Theorem gsumval3OLD 16782
 Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) Obsolete version of gsumval3 16785 as of 31-May-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
gsumval3.b
gsumval3.0
gsumval3.p
gsumval3.z Cntz
gsumval3.g
gsumval3.a
gsumval3.f
gsumval3.c
gsumval3OLD.m
gsumval3OLD.h
gsumval3OLD.n
gsumval3OLD.w
Assertion
Ref Expression
gsumval3OLD g

Proof of Theorem gsumval3OLD
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 15879 . . . . 5 g
51, 2, 4syl2anc 661 . . . 4 g
65adantr 465 . . 3 g
7 gsumval3.f . . . . . . 7
87feqmptd 5911 . . . . . 6
98adantr 465 . . . . 5
10 gsumval3OLD.h . . . . . . . . . . . . . 14
11 f1f 5771 . . . . . . . . . . . . . 14
1210, 11syl 16 . . . . . . . . . . . . 13
1312ad2antrr 725 . . . . . . . . . . . 12
14 f1f1orn 5817 . . . . . . . . . . . . . . . . 17
1510, 14syl 16 . . . . . . . . . . . . . . . 16
1615adantr 465 . . . . . . . . . . . . . . 15
17 f1ocnv 5818 . . . . . . . . . . . . . . 15
1816, 17syl 16 . . . . . . . . . . . . . 14
19 f1of 5806 . . . . . . . . . . . . . 14
2018, 19syl 16 . . . . . . . . . . . . 13
2120ffvelrnda 6016 . . . . . . . . . . . 12
22 fvco3 5935 . . . . . . . . . . . 12
2313, 21, 22syl2anc 661 . . . . . . . . . . 11
24 simpr 461 . . . . . . . . . . . . . . . 16
2524difeq2d 3607 . . . . . . . . . . . . . . 15
26 dif0 3884 . . . . . . . . . . . . . . 15
2725, 26syl6eq 2500 . . . . . . . . . . . . . 14
2827adantr 465 . . . . . . . . . . . . 13
2921, 28eleqtrrd 2534 . . . . . . . . . . . 12
30 fco 5731 . . . . . . . . . . . . . . 15
317, 12, 30syl2anc 661 . . . . . . . . . . . . . 14
3231adantr 465 . . . . . . . . . . . . 13
33 gsumval3OLD.w . . . . . . . . . . . . . . 15
3433eqimss2i 3544 . . . . . . . . . . . . . 14
3534a1i 11 . . . . . . . . . . . . 13
3632, 35suppssrOLD 6006 . . . . . . . . . . . 12
3729, 36syldan 470 . . . . . . . . . . 11
38 f1ocnvfv2 6168 . . . . . . . . . . . . 13
3916, 38sylan 471 . . . . . . . . . . . 12
4039fveq2d 5860 . . . . . . . . . . 11
4123, 37, 403eqtr3rd 2493 . . . . . . . . . 10
42 fvex 5866 . . . . . . . . . . 11
4342elsnc 4038 . . . . . . . . . 10
4441, 43sylibr 212 . . . . . . . . 9
4544adantlr 714 . . . . . . . 8
46 eldif 3471 . . . . . . . . . . 11
47 gsumval3OLD.n . . . . . . . . . . . . 13
487, 47suppssrOLD 6006 . . . . . . . . . . . 12
4948, 43sylibr 212 . . . . . . . . . . 11
5046, 49sylan2br 476 . . . . . . . . . 10
5150adantlr 714 . . . . . . . . 9
5251anassrs 648 . . . . . . . 8
5345, 52pm2.61dan 791 . . . . . . 7
5453, 43sylib 196 . . . . . 6
5554mpteq2dva 4523 . . . . 5
569, 55eqtrd 2484 . . . 4
5756oveq2d 6297 . . 3 g g
58 gsumval3.b . . . . . . . 8
5958, 3mndidcl 15812 . . . . . . 7
601, 59syl 16 . . . . . 6
61 gsumval3.p . . . . . . 7
6258, 61, 3mndlid 15815 . . . . . 6
631, 60, 62syl2anc 661 . . . . 5
6463adantr 465 . . . 4
65 gsumval3OLD.m . . . . . 6
66 nnuz 11125 . . . . . 6
6765, 66syl6eleq 2541 . . . . 5
6867adantr 465 . . . 4
6927eleq2d 2513 . . . . . 6
7069biimpar 485 . . . . 5
7132, 35suppssrOLD 6006 . . . . 5
7270, 71syldan 470 . . . 4
7364, 68, 72seqid3 12130 . . 3
746, 57, 733eqtr4d 2494 . 2 g
75 fzf 11685 . . . . 5
76 ffn 5721 . . . . 5
77 ovelrn 6436 . . . . 5
7875, 76, 77mp2b 10 . . . 4
791ad2antrr 725 . . . . . . . . 9
80 simpr 461 . . . . . . . . . . 11
81 frel 5724 . . . . . . . . . . . . . . . . . 18
827, 81syl 16 . . . . . . . . . . . . . . . . 17
83 reldm0 5210 . . . . . . . . . . . . . . . . 17
8482, 83syl 16 . . . . . . . . . . . . . . . 16
85 fdm 5725 . . . . . . . . . . . . . . . . . 18
867, 85syl 16 . . . . . . . . . . . . . . . . 17
8786eqeq1d 2445 . . . . . . . . . . . . . . . 16
8884, 87bitrd 253 . . . . . . . . . . . . . . 15
89 coeq1 5150 . . . . . . . . . . . . . . . . . . . . 21
90 co01 5512 . . . . . . . . . . . . . . . . . . . . 21
9189, 90syl6eq 2500 . . . . . . . . . . . . . . . . . . . 20
9291cnveqd 5168 . . . . . . . . . . . . . . . . . . 19
93 cnv0 5399 . . . . . . . . . . . . . . . . . . 19
9492, 93syl6eq 2500 . . . . . . . . . . . . . . . . . 18
9594imaeq1d 5326 . . . . . . . . . . . . . . . . 17
96 0ima 5343 . . . . . . . . . . . . . . . . 17
9795, 96syl6eq 2500 . . . . . . . . . . . . . . . 16
9833, 97syl5eq 2496 . . . . . . . . . . . . . . 15
9988, 98syl6bir 229 . . . . . . . . . . . . . 14
10099necon3d 2667 . . . . . . . . . . . . 13
101100imp 429 . . . . . . . . . . . 12
102101adantr 465 . . . . . . . . . . 11
10380, 102eqnetrrd 2737 . . . . . . . . . 10
104 fzn0 11709 . . . . . . . . . 10
105103, 104sylib 196 . . . . . . . . 9
1067ad2antrr 725 . . . . . . . . . 10
10780feq2d 5708 . . . . . . . . . 10
108106, 107mpbid 210 . . . . . . . . 9
10958, 61, 79, 105, 108gsumval2 15781 . . . . . . . 8 g
110 frn 5727 . . . . . . . . . . . . . . 15
11112, 110syl 16 . . . . . . . . . . . . . 14
112111ad2antrr 725 . . . . . . . . . . . . 13
113112, 80sseqtrd 3525 . . . . . . . . . . . 12
114 fzssuz 11733 . . . . . . . . . . . . 13
115 uzssz 11109 . . . . . . . . . . . . . 14
116 zssre 10877 . . . . . . . . . . . . . 14
117115, 116sstri 3498 . . . . . . . . . . . . 13
118114, 117sstri 3498 . . . . . . . . . . . 12
119113, 118syl6ss 3501 . . . . . . . . . . 11
120 ltso 9668 . . . . . . . . . . 11
121 soss 4808 . . . . . . . . . . 11
122119, 120, 121mpisyl 18 . . . . . . . . . 10
123 fzfi 12061 . . . . . . . . . . . 12
124123a1i 11 . . . . . . . . . . . . . . 15
125 fex2 6740 . . . . . . . . . . . . . . 15
12612, 124, 2, 125syl3anc 1229 . . . . . . . . . . . . . 14
127 f1oen3g 7533 . . . . . . . . . . . . . 14
128126, 15, 127syl2anc 661 . . . . . . . . . . . . 13
129 enfi 7738 . . . . . . . . . . . . 13
130128, 129syl 16 . . . . . . . . . . . 12
131123, 130mpbii 211 . . . . . . . . . . 11
132131ad2antrr 725 . . . . . . . . . 10
133 fz1iso 12490 . . . . . . . . . 10
134122, 132, 133syl2anc 661 . . . . . . . . 9
13565nnnn0d 10858 . . . . . . . . . . . . . . . 16
136 hashfz1 12398 . . . . . . . . . . . . . . . 16
137135, 136syl 16 . . . . . . . . . . . . . . 15
138 hashen 12399 . . . . . . . . . . . . . . . . 17
139123, 131, 138sylancr 663 . . . . . . . . . . . . . . . 16
140128, 139mpbird 232 . . . . . . . . . . . . . . 15
141137, 140eqtr3d 2486 . . . . . . . . . . . . . 14
142141ad2antrr 725 . . . . . . . . . . . . 13
143142fveq2d 5860 . . . . . . . . . . . 12
1441ad2antrr 725 . . . . . . . . . . . . . 14
14558, 61mndcl 15803 . . . . . . . . . . . . . . 15
1461453expb 1198 . . . . . . . . . . . . . 14
147144, 146sylan 471 . . . . . . . . . . . . 13
148 gsumval3.c . . . . . . . . . . . . . . . . 17
149148ad2antrr 725 . . . . . . . . . . . . . . . 16
150149sselda 3489 . . . . . . . . . . . . . . 15
151 gsumval3.z . . . . . . . . . . . . . . . 16 Cntz
15261, 151cntzi 16241 . . . . . . . . . . . . . . 15
153150, 152sylan 471 . . . . . . . . . . . . . 14
154153anasss 647 . . . . . . . . . . . . 13
15558, 61mndass 15804 . . . . . . . . . . . . . 14
156144, 155sylan 471 . . . . . . . . . . . . 13
15767ad2antrr 725 . . . . . . . . . . . . 13
1587ad2antrr 725 . . . . . . . . . . . . . 14
159 frn 5727 . . . . . . . . . . . . . 14
160158, 159syl 16 . . . . . . . . . . . . 13
161 simprr 757 . . . . . . . . . . . . . . . . 17
162 isof1o 6206 . . . . . . . . . . . . . . . . 17
163161, 162syl 16 . . . . . . . . . . . . . . . 16
164142oveq2d 6297 . . . . . . . . . . . . . . . . 17
165 f1oeq2 5798 . . . . . . . . . . . . . . . . 17
166164, 165syl 16 . . . . . . . . . . . . . . . 16
167163, 166mpbird 232 . . . . . . . . . . . . . . 15
168 f1ocnv 5818 . . . . . . . . . . . . . . 15
169167, 168syl 16 . . . . . . . . . . . . . 14
17015ad2antrr 725 . . . . . . . . . . . . . 14
171 f1oco 5828 . . . . . . . . . . . . . 14
172169, 170, 171syl2anc 661 . . . . . . . . . . . . 13
173 ffn 5721 . . . . . . . . . . . . . . . . . 18
174 dffn4 5791 . . . . . . . . . . . . . . . . . 18
175173, 174sylib 196 . . . . . . . . . . . . . . . . 17
176158, 175syl 16 . . . . . . . . . . . . . . . 16
177 fof 5785 . . . . . . . . . . . . . . . 16
178176, 177syl 16 . . . . . . . . . . . . . . 15
179 f1of 5806 . . . . . . . . . . . . . . . . 17
180167, 179syl 16 . . . . . . . . . . . . . . . 16
181111ad2antrr 725 . . . . . . . . . . . . . . . 16
182 fss 5729 . . . . . . . . . . . . . . . 16
183180, 181, 182syl2anc 661 . . . . . . . . . . . . . . 15
184 fco 5731 . . . . . . . . . . . . . . 15
185178, 183, 184syl2anc 661 . . . . . . . . . . . . . 14
186185ffvelrnda 6016 . . . . . . . . . . . . 13
187 f1ococnv2 5832 . . . . . . . . . . . . . . . . . . . . . 22
188167, 187syl 16 . . . . . . . . . . . . . . . . . . . . 21
189188coeq1d 5154 . . . . . . . . . . . . . . . . . . . 20
190 f1of 5806 . . . . . . . . . . . . . . . . . . . . . 22
191170, 190syl 16 . . . . . . . . . . . . . . . . . . . . 21
192 fcoi2 5750 . . . . . . . . . . . . . . . . . . . . 21
193191, 192syl 16 . . . . . . . . . . . . . . . . . . . 20
194189, 193eqtr2d 2485 . . . . . . . . . . . . . . . . . . 19
195 coass 5516 . . . . . . . . . . . . . . . . . . 19
196194, 195syl6eq 2500 . . . . . . . . . . . . . . . . . 18
197196coeq2d 5155 . . . . . . . . . . . . . . . . 17
198 coass 5516 . . . . . . . . . . . . . . . . 17
199197, 198syl6eqr 2502 . . . . . . . . . . . . . . . 16
200199fveq1d 5858 . . . . . . . . . . . . . . 15
201200adantr 465 . . . . . . . . . . . . . 14
202 f1of 5806 . . . . . . . . . . . . . . . . 17
203169, 202syl 16 . . . . . . . . . . . . . . . 16
204 fco 5731 . . . . . . . . . . . . . . . 16
205203, 191, 204syl2anc 661 . . . . . . . . . . . . . . 15
206 fvco3 5935 . . . . . . . . . . . . . . 15
207205, 206sylan 471 . . . . . . . . . . . . . 14
208201, 207eqtrd 2484 . . . . . . . . . . . . 13
209147, 154, 156, 157, 160, 172, 186, 208seqf1o 12127 . . . . . . . . . . . 12
21058, 61, 3mndlid 15815 . . . . . . . . . . . . . 14
211144, 210sylan 471 . . . . . . . . . . . . 13
21258, 61, 3mndrid 15816 . . . . . . . . . . . . . 14
213144, 212sylan 471 . . . . . . . . . . . . 13
214144, 59syl 16 . . . . . . . . . . . . 13
215 fdm 5725 . . . . . . . . . . . . . . . . 17
21612, 215syl 16 . . . . . . . . . . . . . . . 16
217 eluzfz1 11702 . . . . . . . . . . . . . . . . . 18
21867, 217syl 16 . . . . . . . . . . . . . . . . 17
219 ne0i 3776 . . . . . . . . . . . . . . . . 17
220218, 219syl 16 . . . . . . . . . . . . . . . 16
221216, 220eqnetrd 2736 . . . . . . . . . . . . . . 15
222 dm0rn0 5209 . . . . . . . . . . . . . . . 16
223222necon3bii 2711 . . . . . . . . . . . . . . 15
224221, 223sylib 196 . . . . . . . . . . . . . 14
225224ad2antrr 725 . . . . . . . . . . . . 13
226113adantrr 716 . . . . . . . . . . . . 13
227 simprl 756 . . . . . . . . . . . . . . . 16
228227eleq2d 2513 . . . . . . . . . . . . . . 15
229228biimpar 485 . . . . . . . . . . . . . 14
230158ffvelrnda 6016 . . . . . . . . . . . . . 14
231229, 230syldan 470 . . . . . . . . . . . . 13
232227difeq1d 3606 . . . . . . . . . . . . . . . 16
233232eleq2d 2513 . . . . . . . . . . . . . . 15
234233biimpar 485 . . . . . . . . . . . . . 14
235 simpll 753 . . . . . . . . . . . . . . 15
236235, 48sylan 471 . . . . . . . . . . . . . 14
237234, 236syldan 470 . . . . . . . . . . . . 13
238 f1of 5806 . . . . . . . . . . . . . . 15
239163, 238syl 16 . . . . . . . . . . . . . 14
240 fvco3 5935 . . . . . . . . . . . . . 14
241239, 240sylan 471 . . . . . . . . . . . . 13
242211, 213, 147, 214, 161, 225, 226, 231, 237, 241seqcoll2 12492 . . . . . . . . . . . 12
243143, 209, 2423eqtr4d 2494 . . . . . . . . . . 11
244243expr 615 . . . . . . . . . 10
245244exlimdv 1711 . . . . . . . . 9
246134, 245mpd 15 . . . . . . . 8
247109, 246eqtr4d 2487 . . . . . . 7 g
248247ex 434 . . . . . 6 g
249248rexlimdvw 2938 . . . . 5 g
250249rexlimdvw 2938 . . . 4 g
25178, 250syl5bi 217 . . 3 g
252 cnvimass 5347 . . . . . . . . . . 11
25333, 252eqsstri 3519 . . . . . . . . . 10
254 fdm 5725 . . . . . . . . . . 11
25531, 254syl 16 . . . . . . . . . 10
256253, 255syl5sseq 3537 . . . . . . . . 9
257 fzssuz 11733 . . . . . . . . . . 11
258257, 66sseqtr4i 3522 . . . . . . . . . 10
259 nnssre 10546 . . . . . . . . . 10
260258, 259sstri 3498 . . . . . . . . 9
261256, 260syl6ss 3501 . . . . . . . 8
262 soss 4808 . . . . . . . 8
263261, 120, 262mpisyl 18 . . . . . . 7
264 ssfi 7742 . . . . . . . 8
265123, 256, 264sylancr 663 . . . . . . 7
266 fz1iso 12490 . . . . . . 7
267263, 265, 266syl2anc 661 . . . . . 6
268267ad2antrr 725 . . . . 5
269 vex 3098 . . . . . . . . . . . 12
270 coexg 6736 . . . . . . . . . . . 12
271126, 269, 270sylancl 662 . . . . . . . . . . 11
272271ad2antrr 725 . . . . . . . . . 10
27310ad2antrr 725 . . . . . . . . . . . . . . . 16
274256ad2antrr 725 . . . . . . . . . . . . . . . 16
275 f1ores 5820 . . . . . . . . . . . . . . . 16
276273, 274, 275syl2anc 661 . . . . . . . . . . . . . . 15
277 cnvco 5178 . . . . . . . . . . . . . . . . . . . 20
278277imaeq1i 5324 . . . . . . . . . . . . . . . . . . 19
279 imaco 5502 . . . . . . . . . . . . . . . . . . 19
28033, 278, 2793eqtri 2476 . . . . . . . . . . . . . . . . . 18
281280imaeq2i 5325 . . . . . . . . . . . . . . . . 17
282273, 14syl 16 . . . . . . . . . . . . . . . . . . 19
283 f1ofo 5813 . . . . . . . . . . . . . . . . . . 19
284282, 283syl 16 . . . . . . . . . . . . . . . . . 18
28547ad2antrr 725 . . . . . . . . . . . . . . . . . 18
286 foimacnv 5823 . . . . . . . . . . . . . . . . . 18
287284, 285, 286syl2anc 661 . . . . . . . . . . . . . . . . 17
288281, 287syl5eq 2496 . . . . . . . . . . . . . . . 16
289 f1oeq3 5799 . . . . . . . . . . . . . . . 16
290288, 289syl 16 . . . . . . . . . . . . . . 15
291276, 290mpbid 210 . . . . . . . . . . . . . 14
292 simprr 757 . . . . . . . . . . . . . . 15
293 isof1o 6206 . . . . . . . . . . . . . . 15
294292, 293syl 16 . . . . . . . . . . . . . 14
295 f1oco 5828 . . . . . . . . . . . . . 14
296291, 294, 295syl2anc 661 . . . . . . . . . . . . 13
297 f1of 5806 . . . . . . . . . . . . . . 15
298294, 297syl 16 . . . . . . . . . . . . . 14
299 frn 5727 . . . . . . . . . . . . . 14
300 cores 5500 . . . . . . . . . . . . . 14
301 f1oeq1 5797 . . . . . . . . . . . . . 14
302298, 299, 300, 3014syl 21 . . . . . . . . . . . . 13
303296, 302mpbid 210 . . . . . . . . . . . 12
304 resexg 5306 . . . . . . . . . . . . . . . . . 18
305126, 304syl 16 . . . . . . . . . . . . . . . . 17
306305ad2antrr 725 . . . . . . . . . . . . . . . 16
307 f1oen3g 7533 . . . . . . . . . . . . . . . 16
308306, 291, 307syl2anc 661 . . . . . . . . . . . . . . 15
309265ad2antrr 725 . . . . . . . . . . . . . . . 16
310 ssfi 7742 . . . . . . . . . . . . . . . . . 18
311131, 47, 310syl2anc 661 . . . . . . . . . . . . . . . . 17
312311ad2antrr 725 . . . . . . . . . . . . . . . 16
313 hashen 12399 . . . . . . . . . . . . . . . 16
314309, 312, 313syl2anc 661 . . . . . . . . . . . . . . 15
315308, 314mpbird 232 . . . . . . . . . . . . . 14
316315oveq2d 6297 . . . . . . . . . . . . 13
317 f1oeq2 5798 . . . . . . . . . . . . 13
318316, 317syl 16 . . . . . . . . . . . 12
319303, 318mpbid 210 . . . . . . . . . . 11
320315fveq2d 5860 . . . . . . . . . . 11
321319, 320jca 532 . . . . . . . . . 10
322 f1oeq1 5797 . . . . . . . . . . . 12
323 coeq2 5151 . . . . . . . . . . . . . . 15
324323seqeq3d 12094 . . . . . . . . . . . . . 14
325324fveq1d 5858 . . . . . . . . . . . . 13
326325eqeq2d 2457 . . . . . . . . . . . 12
327322, 326anbi12d 710 . . . . . . . . . . 11
328327spcegv 3181 . . . . . . . . . 10
329272, 321, 328sylc 60 . . . . . . . . 9
3301ad2antrr 725 . . . . . . . . . . . . . 14
3312ad2antrr 725 . . . . . . . . . . . . . 14
3327ad2antrr 725 . . . . . . . . . . . . . 14
333148ad2antrr 725 . . . . . . . . . . . . . 14
334 imaeq2 5323 . . . . . . . . . . . . . . . . . 18
335 ima0 5342 . . . . . . . . . . . . . . . . . 18
336334, 335syl6eq 2500 . . . . . . . . . . . . . . . . 17
337280, 336syl5eq 2496 . . . . . . . . . . . . . . . 16
338337necon3i 2683 . . . . . . . . . . . . . . 15
339338ad2antlr 726 . . . . . . . . . . . . . 14
340111ad2antrr 725 . . . . . . . . . . . . . . 15
341285, 340sstrd 3499 . . . . . . . . . . . . . 14
34258, 3, 61, 151, 330, 331, 332, 333, 312, 339, 341gsumval3eu 16781 . . . . . . . . . . . . 13
343 iota1 5555 . . . . . . . . . . . . 13
344342, 343syl 16 . . . . . . . . . . . 12
345 eqid 2443 . . . . . . . . . . . . . 14
346 simprl 756 . . . . . . . . . . . . . 14
34758, 3, 61, 151, 330, 331, 332, 333, 312, 339, 345, 346gsumval3aOLD 16780 . . . . . . . . . . . . 13 g
348347eqeq1d 2445 . . . . . . . . . . . 12 g
349344, 348bitr4d 256 . . . . . . . . . . 11 g
350349alrimiv 1706 . . . . . . . . . 10 g
351 fvex 5866 . . . . . . . . . . 11
352 eqeq1 2447 . . . . . . . . . . . . . 14
353352anbi2d 703 . . . . . . . . . . . . 13
354353exbidv 1701 . . . . . . . . . . . 12
355 eqeq2 2458 . . . . . . . . . . . 12 g g
356354, 355bibi12d 321 . . . . . . . . . . 11 g g
357351, 356spcv 3186 . . . . . . . . . 10 g g
358350, 357syl 16 . . . . . . . . 9 g
359329, 358mpbid 210 . . . . . . . 8 g
360330, 210sylan 471 . . . . . . . . 9
361330, 212sylan 471 . . . . . . . . 9
362330, 146sylan 471 . . . . . . . . 9
363330, 59syl 16 . . . . . . . . 9
364 simplr 755 . . . . . . . . 9
36531ad2antrr 725 . . . . . . . . . 10
366365ffvelrnda 6016 . . . . . . . . 9
36734a1i 11 . . . . . . . . . 10
368365, 367suppssrOLD 6006 . . . . . . . . 9
369 coass 5516 . . . . . . . . . . 11
370369fveq1i 5857 . . . . . . . . . 10