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

Theorem psrass1lem 18678
 Description: A group sum commutation used by psrass1 18706. (Contributed by Mario Carneiro, 5-Jan-2015.)
Hypotheses
Ref Expression
psrbag.d
psrbagconf1o.1
gsumbagdiag.i
gsumbagdiag.f
gsumbagdiag.b
gsumbagdiag.g CMnd
gsumbagdiag.x
psrass1lem.y
Assertion
Ref Expression
psrass1lem g g g g
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,,   ,,,,   ,,   ,,,,   ,,   ,,,,,   ,,,,   ,,,,
Allowed substitution hints:   (,,,)   (,,,)   ()   (,)   (,)   (,,)   (,)   (,)

Proof of Theorem psrass1lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psrbag.d . . . 4
2 psrbagconf1o.1 . . . 4
3 gsumbagdiag.i . . . 4
4 gsumbagdiag.f . . . 4
5 gsumbagdiag.b . . . 4
6 gsumbagdiag.g . . . 4 CMnd
71, 2, 3, 4gsumbagdiaglem 18676 . . . . 5
8 gsumbagdiag.x . . . . . . . . . . . 12
98anassrs 660 . . . . . . . . . . 11
10 eqid 2471 . . . . . . . . . . 11
119, 10fmptd 6061 . . . . . . . . . 10
123adantr 472 . . . . . . . . . . . 12
13 ssrab2 3500 . . . . . . . . . . . . . 14
142, 13eqsstri 3448 . . . . . . . . . . . . 13
154adantr 472 . . . . . . . . . . . . . 14
16 simpr 468 . . . . . . . . . . . . . 14
171, 2psrbagconcl 18674 . . . . . . . . . . . . . 14
1812, 15, 16, 17syl3anc 1292 . . . . . . . . . . . . 13
1914, 18sseldi 3416 . . . . . . . . . . . 12
20 eqid 2471 . . . . . . . . . . . . 13
211, 20psrbagconf1o 18675 . . . . . . . . . . . 12
2212, 19, 21syl2anc 673 . . . . . . . . . . 11
23 f1of 5828 . . . . . . . . . . 11
2422, 23syl 17 . . . . . . . . . 10
25 fco 5751 . . . . . . . . . 10
2611, 24, 25syl2anc 673 . . . . . . . . 9
2712adantr 472 . . . . . . . . . . . . . . . . 17
2815adantr 472 . . . . . . . . . . . . . . . . 17
291psrbagf 18666 . . . . . . . . . . . . . . . . 17
3027, 28, 29syl2anc 673 . . . . . . . . . . . . . . . 16
3130ffvelrnda 6037 . . . . . . . . . . . . . . 15
3216adantr 472 . . . . . . . . . . . . . . . . . 18
3314, 32sseldi 3416 . . . . . . . . . . . . . . . . 17
341psrbagf 18666 . . . . . . . . . . . . . . . . 17
3527, 33, 34syl2anc 673 . . . . . . . . . . . . . . . 16
3635ffvelrnda 6037 . . . . . . . . . . . . . . 15
37 ssrab2 3500 . . . . . . . . . . . . . . . . . 18
38 simpr 468 . . . . . . . . . . . . . . . . . 18
3937, 38sseldi 3416 . . . . . . . . . . . . . . . . 17
401psrbagf 18666 . . . . . . . . . . . . . . . . 17
4127, 39, 40syl2anc 673 . . . . . . . . . . . . . . . 16
4241ffvelrnda 6037 . . . . . . . . . . . . . . 15
43 nn0cn 10903 . . . . . . . . . . . . . . . 16
44 nn0cn 10903 . . . . . . . . . . . . . . . 16
45 nn0cn 10903 . . . . . . . . . . . . . . . 16
46 sub32 9928 . . . . . . . . . . . . . . . 16
4743, 44, 45, 46syl3an 1334 . . . . . . . . . . . . . . 15
4831, 36, 42, 47syl3anc 1292 . . . . . . . . . . . . . 14
4948mpteq2dva 4482 . . . . . . . . . . . . 13
50 ovex 6336 . . . . . . . . . . . . . . 15
5150a1i 11 . . . . . . . . . . . . . 14
5230feqmptd 5932 . . . . . . . . . . . . . . 15
5335feqmptd 5932 . . . . . . . . . . . . . . 15
5427, 31, 36, 52, 53offval2 6567 . . . . . . . . . . . . . 14
5541feqmptd 5932 . . . . . . . . . . . . . 14
5627, 51, 42, 54, 55offval2 6567 . . . . . . . . . . . . 13
57 ovex 6336 . . . . . . . . . . . . . . 15
5857a1i 11 . . . . . . . . . . . . . 14
5927, 31, 42, 52, 55offval2 6567 . . . . . . . . . . . . . 14
6027, 58, 36, 59, 53offval2 6567 . . . . . . . . . . . . 13
6149, 56, 603eqtr4d 2515 . . . . . . . . . . . 12
6219adantr 472 . . . . . . . . . . . . 13
631, 20psrbagconcl 18674 . . . . . . . . . . . . 13
6427, 62, 38, 63syl3anc 1292 . . . . . . . . . . . 12
6561, 64eqeltrrd 2550 . . . . . . . . . . 11
6661mpteq2dva 4482 . . . . . . . . . . 11
67 nfcv 2612 . . . . . . . . . . . . 13
68 nfcsb1v 3365 . . . . . . . . . . . . 13
69 csbeq1a 3358 . . . . . . . . . . . . 13
7067, 68, 69cbvmpt 4487 . . . . . . . . . . . 12
7170a1i 11 . . . . . . . . . . 11
72 csbeq1 3352 . . . . . . . . . . 11
7365, 66, 71, 72fmptco 6072 . . . . . . . . . 10
7473feq1d 5724 . . . . . . . . 9
7526, 74mpbid 215 . . . . . . . 8
76 eqid 2471 . . . . . . . . 9
7776fmpt 6058 . . . . . . . 8
7875, 77sylibr 217 . . . . . . 7
7978r19.21bi 2776 . . . . . 6
8079anasss 659 . . . . 5
817, 80syldan 478 . . . 4
821, 2, 3, 4, 5, 6, 81gsumbagdiag 18677 . . 3 g g
83 eqid 2471 . . . 4
841psrbaglefi 18673 . . . . . 6
853, 4, 84syl2anc 673 . . . . 5
862, 85syl5eqel 2553 . . . 4
873adantr 472 . . . . 5
884adantr 472 . . . . . . 7
89 simpr 468 . . . . . . 7
901, 2psrbagconcl 18674 . . . . . . 7
9187, 88, 89, 90syl3anc 1292 . . . . . 6
9214, 91sseldi 3416 . . . . 5
931psrbaglefi 18673 . . . . 5
9487, 92, 93syl2anc 673 . . . 4
95 xpfi 7860 . . . . 5
9686, 86, 95syl2anc 673 . . . 4
97 simprl 772 . . . . . . 7
987simpld 466 . . . . . . 7
99 brxp 4870 . . . . . . 7
10097, 98, 99sylanbrc 677 . . . . . 6
101100pm2.24d 139 . . . . 5
102101impr 631 . . . 4
1035, 83, 6, 86, 94, 81, 96, 102gsum2d2 17684 . . 3 g g g
1041psrbaglefi 18673 . . . . 5
10512, 19, 104syl2anc 673 . . . 4
106 simprl 772 . . . . . . 7
1071, 2, 3, 4gsumbagdiaglem 18676 . . . . . . . 8
108107simpld 466 . . . . . . 7
109 brxp 4870 . . . . . . 7
110106, 108, 109sylanbrc 677 . . . . . 6
111110pm2.24d 139 . . . . 5
112111impr 631 . . . 4
1135, 83, 6, 86, 105, 80, 96, 112gsum2d2 17684 . . 3 g g g
11482, 103, 1133eqtr3d 2513 . 2 g g g g
1156adantr 472 . . . . . . . 8 CMnd
11681anassrs 660 . . . . . . . . 9
117 eqid 2471 . . . . . . . . 9
118116, 117fmptd 6061 . . . . . . . 8
119 ovex 6336 . . . . . . . . . . . 12
1201, 119rabex2 4552 . . . . . . . . . . 11
121120a1i 11 . . . . . . . . . 10
122 rabexg 4549 . . . . . . . . . 10
123 mptexg 6151 . . . . . . . . . 10
124121, 122, 1233syl 18 . . . . . . . . 9
125 funmpt 5625 . . . . . . . . . 10
126125a1i 11 . . . . . . . . 9
127 fvex 5889 . . . . . . . . . 10
128127a1i 11 . . . . . . . . 9
129 suppssdm 6946 . . . . . . . . . . 11 supp
130117dmmptss 5338 . . . . . . . . . . 11
131129, 130sstri 3427 . . . . . . . . . 10 supp
132131a1i 11 . . . . . . . . 9 supp
133 suppssfifsupp 7916 . . . . . . . . 9 supp finSupp
134124, 126, 128, 94, 132, 133syl32anc 1300 . . . . . . . 8 finSupp
1355, 83, 115, 94, 118, 134gsumcl 17627 . . . . . . 7 g
136 eqid 2471 . . . . . . 7 g g
137135, 136fmptd 6061 . . . . . 6 g
1381, 2psrbagconf1o 18675 . . . . . . . 8
1393, 4, 138syl2anc 673 . . . . . . 7
140 f1ocnv 5840 . . . . . . 7
141 f1of 5828 . . . . . . 7
142139, 140, 1413syl 18 . . . . . 6
143 fco 5751 . . . . . 6 g g
144137, 142, 143syl2anc 673 . . . . 5 g
145 coass 5361 . . . . . . . 8 g g
146 f1ococnv2 5854 . . . . . . . . . 10
147139, 146syl 17 . . . . . . . . 9
148147coeq2d 5002 . . . . . . . 8 g g
149145, 148syl5eq 2517 . . . . . . 7 g g
150 eqidd 2472 . . . . . . . . 9
151 eqidd 2472 . . . . . . . . 9 g g
152 breq2 4399 . . . . . . . . . . . 12
153152rabbidv 3022 . . . . . . . . . . 11
154 ovex 6336 . . . . . . . . . . . . 13
155 psrass1lem.y . . . . . . . . . . . . 13
156154, 155csbie 3375 . . . . . . . . . . . 12
157 oveq1 6315 . . . . . . . . . . . . 13
158157csbeq1d 3356 . . . . . . . . . . . 12
159156, 158syl5eqr 2519 . . . . . . . . . . 11
160153, 159mpteq12dv 4474 . . . . . . . . . 10
161160oveq2d 6324 . . . . . . . . 9 g g
16291, 150, 151, 161fmptco 6072 . . . . . . . 8 g g
163162coeq1d 5001 . . . . . . 7 g g
164 coires1 5360 . . . . . . . . 9 g g
165 ssid 3437 . . . . . . . . . 10
166 resmpt 5160 . . . . . . . . . 10 g g
167165, 166ax-mp 5 . . . . . . . . 9 g g
168164, 167eqtri 2493 . . . . . . . 8 g g
169168a1i 11 . . . . . . 7 g g
170149, 163, 1693eqtr3d 2513 . . . . . 6 g g
171170feq1d 5724 . . . . 5 g g
172144, 171mpbid 215 . . . 4 g
173 rabexg 4549 . . . . . . . 8
174120, 173mp1i 13 . . . . . . 7
1752, 174syl5eqel 2553 . . . . . 6
176 mptexg 6151 . . . . . 6 g
177175, 176syl 17 . . . . 5 g
178 funmpt 5625 . . . . . 6 g
179178a1i 11 . . . . 5 g
180127a1i 11 . . . . 5
181 suppssdm 6946 . . . . . . 7 g supp g
182 eqid 2471 . . . . . . . 8 g g
183182dmmptss 5338 . . . . . . 7 g
184181, 183sstri 3427 . . . . . 6 g supp
185184a1i 11 . . . . 5 g supp
186 suppssfifsupp 7916 . . . . 5 g g g supp g finSupp
187177, 179, 180, 86, 185, 186syl32anc 1300 . . . 4 g finSupp
1885, 83, 6, 86, 172, 187, 139gsumf1o 17628 . . 3 g g g g
189162oveq2d 6324 . . 3 g g g g
190188, 189eqtrd 2505 . 2 g g g g
1916adantr 472 . . . . . 6 CMnd
192120a1i 11 . . . . . . . 8
193 rabexg 4549 . . . . . . . 8
194 mptexg 6151 . . . . . . . 8
195192, 193, 1943syl 18 . . . . . . 7
196 funmpt 5625 . . . . . . . 8
197196a1i 11 . . . . . . 7
198127a1i 11 . . . . . . 7
199 suppssdm 6946 . . . . . . . . 9 supp
20010dmmptss 5338 . . . . . . . . 9
201199, 200sstri 3427 . . . . . . . 8 supp
202201a1i 11 . . . . . . 7 supp
203 suppssfifsupp 7916 . . . . . . 7 supp finSupp
204195, 197, 198, 105, 202, 203syl32anc 1300 . . . . . 6 finSupp
2055, 83, 191, 105, 11, 204, 22gsumf1o 17628 . . . . 5 g g
20673oveq2d 6324 . . . . 5 g g
207205, 206eqtrd 2505 . . . 4 g g
208207mpteq2dva 4482 . . 3 g g
209208oveq2d 6324 . 2 g g g g
210114, 190, 2093eqtr4d 2515 1 g g g g
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 376   wceq 1452   wcel 1904  wral 2756  crab 2760  cvv 3031  csb 3349   wss 3390   class class class wbr 4395   cmpt 4454   cid 4749   cxp 4837  ccnv 4838   cdm 4839   cres 4841  cima 4842   ccom 4843   wfun 5583  wf 5585  wf1o 5588  cfv 5589  (class class class)co 6308   cmpt2 6310   cof 6548   cofr 6549   supp csupp 6933   cmap 7490  cfn 7587   finSupp cfsupp 7901  cc 9555   cle 9694   cmin 9880  cn 10631  cn0 10893  cbs 15199  c0g 15416   g cgsu 15417  CMndccmn 17508 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-inf2 8164  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-iin 4272  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-of 6550  df-ofr 6551  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-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  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-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-fzo 11943  df-seq 12252  df-hash 12554  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-0g 15418  df-gsum 15419  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-mulg 16754  df-cntz 17049  df-cmn 17510 This theorem is referenced by:  psrass1  18706
 Copyright terms: Public domain W3C validator