Theorem gsum0 18643

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.

Step	Hyp	Ref	Expression
1		eqid 2739	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		gsum0.z	. . 3 ⊢ 0 = (0g‘𝐺)
3		eqid 2739	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
4		eqid 2739	. . 3 ⊢ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} = {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
5		id 22	. . 3 ⊢ (𝐺 ∈ V → 𝐺 ∈ V)
6		0ex 5229	. . . 4 ⊢ ∅ ∈ V
7	6	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅ ∈ V)
8		f0 6708	. . . 4 ⊢ ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
9	8	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)})
10	1, 2, 3, 4, 5, 7, 9	gsumval1 18642	. 2 ⊢ (𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
11		df-gsum 17396	. . . . 5 ⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))))))
12	11	reldmmpo 7490	. . . 4 ⊢ Rel dom Σg
13	12	ovprc1 7395	. . 3 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = ∅)
14		fvprc 6819	. . . 4 ⊢ (¬ 𝐺 ∈ V → (0g‘𝐺) = ∅)
15	2, 14	eqtrid 2786	. . 3 ⊢ (¬ 𝐺 ∈ V → 0 = ∅)
16	13, 15	eqtr4d 2777	. 2 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
17	10, 16	pm2.61i 183	1 ⊢ (𝐺 Σg ∅) = 0

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063  {crab 3391  Vcvv 3431  [wsbc 3723  ⦋csb 3831   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4261  ifcif 4454  ^◡ccnv 5617  dom cdm 5618  ran crn 5619   “ cima 5621   ∘ ccom 5622  ℩cio 6439  ⟶wf 6481  –1-1-onto→wf1o 6484  ‘cfv 6485  (class class class)co 7356  1c1 11030  ℤ_≥cuz 12779  ...cfz 13452  seqcseq 13954  ♯chash 14283  Basecbs 17170  +_gcplusg 17211  0_gc0g 17393   Σ_g cgsu 17394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-seq 13955  df-gsum 17396

This theorem is referenced by:  gsumwsubmcl  18796  gsumccat  18800  gsumwmhm  18804  gsumwspan  18805  frmdgsum  18821  frmdup1  18823  mulgnn0gsum  19047  gsumwrev  19332  gsmsymgrfix  19394  gsmsymgreq  19398  psgnunilem2  19461  psgn0fv0  19477  psgnsn  19486  psgnprfval1  19488  gsumconst  19900  gsumle  20111  gsumfsum  21409  mplmonmul  22012  mplcoe1  22013  mplcoe5  22016  coe1fzgsumd  22290  evl1gsumd  22343  mdet0pr  22575  madugsum  22626  tmdgsum  24078  xrge0gsumle  24817  xrge0tsms  24818  jensen  26970  suppgsumssiun  33153  xrge0tsmsd  33154  gsumwun  33157  cyc3genpmlem  33232  gsumvsca1  33307  gsumvsca2  33308  elrgspnlem2  33324  elrgspnlem4  33326  domnprodn0  33356  domnprodeq0  33357  unitprodclb  33472  rprmdvdsprod  33617  1arithidom  33620  1arithufdlem3  33629  1arithufdlem4  33630  dfufd2lem  33632  deg1prod  33666  ply1coedeg  33672  psrgsum  33732  psrmonmul  33734  psrmonprod  33736  vieta  33764  zarcmplem  34065  esumnul  34232  esumsnf  34248  sitg0  34530  mrsub0  35744  matunitlindflem1  37983  evl1gprodd  42602  idomnnzgmulnz  42618  deg1gprod  42625  lincval0  48906