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

Theorem gsumzoppg 15218
 Description: The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016.)
Hypotheses
Ref Expression
gsumzoppg.b
gsumzoppg.0
gsumzoppg.z Cntz
gsumzoppg.o oppg
gsumzoppg.g
gsumzoppg.a
gsumzoppg.f
gsumzoppg.c
gsumzoppg.n
Assertion
Ref Expression
gsumzoppg g g

Proof of Theorem gsumzoppg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumzoppg.g . . . . . . . 8
2 gsumzoppg.o . . . . . . . . 9 oppg
32oppgmnd 14829 . . . . . . . 8
41, 3syl 15 . . . . . . 7
5 gsumzoppg.a . . . . . . 7
6 gsumzoppg.0 . . . . . . . . 9
72, 6oppgid 14831 . . . . . . . 8
87gsumz 14460 . . . . . . 7 g
94, 5, 8syl2anc 642 . . . . . 6 g
106gsumz 14460 . . . . . . 7 g
111, 5, 10syl2anc 642 . . . . . 6 g
129, 11eqtr4d 2320 . . . . 5 g g
1312adantr 451 . . . 4 g g
14 gsumzoppg.f . . . . . 6
15 ssid 3199 . . . . . . 7
1615a1i 10 . . . . . 6
1714, 16gsumcllem 15195 . . . . 5
1817oveq2d 5876 . . . 4 g g
1917oveq2d 5876 . . . 4 g g
2013, 18, 193eqtr4d 2327 . . 3 g g
2120ex 423 . 2 g g
22 simprl 732 . . . . . . . 8
23 nnuz 10265 . . . . . . . 8
2422, 23syl6eleq 2375 . . . . . . 7
2514adantr 451 . . . . . . . . . . 11
26 ffn 5391 . . . . . . . . . . . 12
27 dffn4 5459 . . . . . . . . . . . 12
2826, 27sylib 188 . . . . . . . . . . 11
29 fof 5453 . . . . . . . . . . 11
3025, 28, 293syl 18 . . . . . . . . . 10
311adantr 451 . . . . . . . . . . . 12
32 gsumzoppg.b . . . . . . . . . . . . 13
3332submacs 14444 . . . . . . . . . . . 12 SubMnd ACS
34 acsmre 13556 . . . . . . . . . . . 12 SubMnd ACS SubMnd Moore
3531, 33, 343syl 18 . . . . . . . . . . 11 SubMnd Moore
36 frn 5397 . . . . . . . . . . . 12
3725, 36syl 15 . . . . . . . . . . 11
38 eqid 2285 . . . . . . . . . . . 12 mrClsSubMnd mrClsSubMnd
3938mrcssid 13521 . . . . . . . . . . 11 SubMnd Moore mrClsSubMnd
4035, 37, 39syl2anc 642 . . . . . . . . . 10 mrClsSubMnd
41 fss 5399 . . . . . . . . . 10 mrClsSubMnd mrClsSubMnd
4230, 40, 41syl2anc 642 . . . . . . . . 9 mrClsSubMnd
43 f1of1 5473 . . . . . . . . . . . 12
4443ad2antll 709 . . . . . . . . . . 11
45 cnvimass 5035 . . . . . . . . . . . 12
46 fdm 5395 . . . . . . . . . . . . 13
4725, 46syl 15 . . . . . . . . . . . 12
4845, 47syl5sseq 3228 . . . . . . . . . . 11
49 f1ss 5444 . . . . . . . . . . 11
5044, 48, 49syl2anc 642 . . . . . . . . . 10
51 f1f 5439 . . . . . . . . . 10
5250, 51syl 15 . . . . . . . . 9
53 fco 5400 . . . . . . . . 9 mrClsSubMnd mrClsSubMnd
5442, 52, 53syl2anc 642 . . . . . . . 8 mrClsSubMnd
55 ffvelrn 5665 . . . . . . . 8 mrClsSubMnd mrClsSubMnd
5654, 55sylan 457 . . . . . . 7 mrClsSubMnd
5738mrccl 13515 . . . . . . . . . 10 SubMnd Moore mrClsSubMnd SubMnd
5835, 37, 57syl2anc 642 . . . . . . . . 9 mrClsSubMnd SubMnd
592oppgsubm 14837 . . . . . . . . 9 SubMnd SubMnd
6058, 59syl6eleq 2375 . . . . . . . 8 mrClsSubMnd SubMnd
61 eqid 2285 . . . . . . . . . 10
6261submcl 14432 . . . . . . . . 9 mrClsSubMnd SubMnd mrClsSubMnd mrClsSubMnd mrClsSubMnd
63623expb 1152 . . . . . . . 8 mrClsSubMnd SubMnd mrClsSubMnd mrClsSubMnd mrClsSubMnd
6460, 63sylan 457 . . . . . . 7 mrClsSubMnd mrClsSubMnd mrClsSubMnd
65 gsumzoppg.c . . . . . . . . . . . . . 14
6665adantr 451 . . . . . . . . . . . . 13
67 gsumzoppg.z . . . . . . . . . . . . . 14 Cntz
68 eqid 2285 . . . . . . . . . . . . . 14 s mrClsSubMnd s mrClsSubMnd
6967, 38, 68cntzspan 15139 . . . . . . . . . . . . 13 s mrClsSubMnd CMnd
7031, 66, 69syl2anc 642 . . . . . . . . . . . 12 s mrClsSubMnd CMnd
7168, 67submcmn2 15137 . . . . . . . . . . . . 13 mrClsSubMnd SubMnd s mrClsSubMnd CMnd mrClsSubMnd mrClsSubMnd
7258, 71syl 15 . . . . . . . . . . . 12 s mrClsSubMnd CMnd mrClsSubMnd mrClsSubMnd
7370, 72mpbid 201 . . . . . . . . . . 11 mrClsSubMnd mrClsSubMnd
7473sselda 3182 . . . . . . . . . 10 mrClsSubMnd mrClsSubMnd
75 eqid 2285 . . . . . . . . . . 11
7675, 67cntzi 14807 . . . . . . . . . 10 mrClsSubMnd mrClsSubMnd
7774, 76sylan 457 . . . . . . . . 9 mrClsSubMnd mrClsSubMnd
7875, 2, 61oppgplus 14824 . . . . . . . . 9
7977, 78syl6reqr 2336 . . . . . . . 8 mrClsSubMnd mrClsSubMnd
8079anasss 628 . . . . . . 7 mrClsSubMnd mrClsSubMnd
8124, 56, 64, 80seqfeq4 11097 . . . . . 6
822, 32oppgbas 14826 . . . . . . 7
83 eqid 2285 . . . . . . 7 Cntz Cntz
844adantr 451 . . . . . . 7
855adantr 451 . . . . . . 7
862, 67oppgcntz 14839 . . . . . . . 8 Cntz
8766, 86syl6sseq 3226 . . . . . . 7 Cntz
88 f1ofo 5481 . . . . . . . . . 10
89 forn 5456 . . . . . . . . . 10
9088, 89syl 15 . . . . . . . . 9
9190ad2antll 709 . . . . . . . 8
9215, 91syl5sseqr 3229 . . . . . . 7
93 eqid 2285 . . . . . . 7
9482, 7, 61, 83, 84, 85, 25, 87, 22, 50, 92, 93gsumval3 15193 . . . . . 6 g
9532, 6, 75, 67, 31, 85, 25, 66, 22, 50, 92, 93gsumval3 15193 . . . . . 6 g
9681, 94, 953eqtr4d 2327 . . . . 5 g g
9796expr 598 . . . 4 g g
9897exlimdv 1666 . . 3 g g
9998expimpd 586 . 2 g g
100 gsumzoppg.n . . 3
101 fz1f1o 12185 . . 3
102100, 101syl 15 . 2
10321, 99, 102mpjaod 370 1 g g
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wo 357   wa 358  wex 1530   wceq 1625   wcel 1686  cvv 2790   cdif 3151   wss 3154  c0 3457  csn 3642   cmpt 4079  ccnv 4690   cdm 4691   crn 4692  cima 4694   ccom 4695   wfn 5252  wf 5253  wf1 5254  wfo 5255  wf1o 5256  cfv 5257  (class class class)co 5860  cfn 6865  c1 8740  cn 9748  cuz 10232  cfz 10784   cseq 11048  chash 11339  cbs 13150   ↾s cress 13151   cplusg 13210  c0g 13402   g cgsu 13403  Moorecmre 13486  mrClscmrc 13487  ACScacs 13489  cmnd 14363  SubMndcsubmnd 14416  Cntzccntz 14793  oppgcoppg 14820  CMndccmn 15091 This theorem is referenced by:  gsumzinv  15219 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-iin 3910  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-se 4355  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-isom 5266  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-tpos 6236  df-riota 6306  df-recs 6390  df-rdg 6425  df-1o 6481  df-oadd 6485  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-oi 7227  df-card 7574  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-nn 9749  df-2 9806  df-n0 9968  df-z 10027  df-uz 10233  df-fz 10785  df-fzo 10873  df-seq 11049  df-hash 11340  df-ndx 13153  df-slot 13154  df-base 13155  df-sets 13156  df-ress 13157  df-plusg 13223  df-0g 13406  df-gsum 13407  df-mre 13490  df-mrc 13491  df-acs 13493  df-mnd 14369  df-submnd 14418  df-cntz 14795  df-oppg 14821  df-cmn 15093
 Copyright terms: Public domain W3C validator