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

Theorem gsum0 18677
Description: Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.)
Hypothesis
Ref Expression
gsum0.z 0 = (0g𝐺)
Assertion
Ref Expression
gsum0 (𝐺 Σg ∅) = 0

Proof of Theorem gsum0
Dummy variables 𝑓 𝑔 𝑚 𝑛 𝑜 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2726 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 gsum0.z . . 3 0 = (0g𝐺)
3 eqid 2726 . . 3 (+g𝐺) = (+g𝐺)
4 eqid 2726 . . 3 {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g𝐺)𝑦) = 𝑦 ∧ (𝑦(+g𝐺)𝑥) = 𝑦)} = {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g𝐺)𝑦) = 𝑦 ∧ (𝑦(+g𝐺)𝑥) = 𝑦)}
5 id 22 . . 3 (𝐺 ∈ V → 𝐺 ∈ V)
6 0ex 5312 . . . 4 ∅ ∈ V
76a1i 11 . . 3 (𝐺 ∈ V → ∅ ∈ V)
8 f0 6783 . . . 4 ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g𝐺)𝑦) = 𝑦 ∧ (𝑦(+g𝐺)𝑥) = 𝑦)}
98a1i 11 . . 3 (𝐺 ∈ V → ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g𝐺)𝑦) = 𝑦 ∧ (𝑦(+g𝐺)𝑥) = 𝑦)})
101, 2, 3, 4, 5, 7, 9gsumval1 18676 . 2 (𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
11 df-gsum 17457 . . . . 5 Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} / 𝑜if(ran 𝑓𝑜, (0g𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))), (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦)))))))
1211reldmmpo 7560 . . . 4 Rel dom Σg
1312ovprc1 7463 . . 3 𝐺 ∈ V → (𝐺 Σg ∅) = ∅)
14 fvprc 6893 . . . 4 𝐺 ∈ V → (0g𝐺) = ∅)
152, 14eqtrid 2778 . . 3 𝐺 ∈ V → 0 = ∅)
1613, 15eqtr4d 2769 . 2 𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
1710, 16pm2.61i 182 1 (𝐺 Σg ∅) = 0
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 394   = wceq 1534  wex 1774  wcel 2099  wral 3051  wrex 3060  {crab 3419  Vcvv 3462  [wsbc 3776  csb 3892  cdif 3944  wss 3947  c0 4325  ifcif 4533  ccnv 5681  dom cdm 5682  ran crn 5683  cima 5685  ccom 5686  cio 6504  wf 6550  1-1-ontowf1o 6553  cfv 6554  (class class class)co 7424  1c1 11159  cuz 12874  ...cfz 13538  seqcseq 14021  chash 14347  Basecbs 17213  +gcplusg 17266  0gc0g 17454   Σg cgsu 17455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-seq 14022  df-gsum 17457
This theorem is referenced by:  gsumwsubmcl  18827  gsumccat  18831  gsumwmhm  18835  gsumwspan  18836  frmdgsum  18852  frmdup1  18854  mulgnn0gsum  19074  gsumwrev  19363  gsmsymgrfix  19426  gsmsymgreq  19430  psgnunilem2  19493  psgn0fv0  19509  psgnsn  19518  psgnprfval1  19520  gsumconst  19932  gsumfsum  21431  mplmonmul  22043  mplcoe1  22044  mplcoe5  22047  coe1fzgsumd  22295  evl1gsumd  22348  mdet0pr  22585  madugsum  22636  tmdgsum  24090  xrge0gsumle  24840  xrge0tsms  24841  jensen  27017  xrge0tsmsd  32926  gsumle  32959  cyc3genpmlem  33029  gsumvsca1  33090  gsumvsca2  33091  domnprodn0  33130  unitprodclb  33264  rprmdvdsprod  33409  1arithidom  33412  1arithufdlem3  33421  1arithufdlem4  33422  dfufd2lem  33424  zarcmplem  33696  esumnul  33881  esumsnf  33897  sitg0  34180  mrsub0  35344  matunitlindflem1  37317  evl1gprodd  41815  idomnnzgmulnz  41831  deg1gprod  41838  lincval0  47798
  Copyright terms: Public domain W3C validator