Theorem gsum0 18786

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 2760	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		gsum0.z	. . 3 ⊢ 0 = (0g‘𝐺)
3		eqid 2760	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
4		eqid 2760	. . 3 ⊢ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} = {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
5		id 23	. . 3 ⊢ (𝐺 ∈ V → 𝐺 ∈ V)
6		0ex 5264	. . . 4 ⊢ ∅ ∈ V
7	6	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅ ∈ V)
8		f0 6756	. . . 4 ⊢ ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
9	8	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)})
10	1, 2, 3, 4, 5, 7, 9	gsumval1 18785	. 2 ⊢ (𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
11		df-gsum 17527	. . . . 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 7547	. . . 4 ⊢ Rel dom Σg
13	12	ovprc1 7452	. . 3 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = ∅)
14		fvprc 6870	. . . 4 ⊢ (¬ 𝐺 ∈ V → (0g‘𝐺) = ∅)
15	2, 14	eqtrid 2807	. . 3 ⊢ (¬ 𝐺 ∈ V → 0 = ∅)
16	13, 15	eqtr4d 2798	. 2 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
17	10, 16	pm2.61i 184	1 ⊢ (𝐺 Σg ∅) = 0

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450  [wsbc 3739  ⦋csb 3847   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4279  ifcif 4482  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658   ∘ ccom 5659  ℩cio 6487  ⟶wf 6529  –1-1-onto→wf1o 6532  ‘cfv 6533  (class class class)co 7413  1c1 11125  ℤ_≥cuz 12887  ...cfz 13561  seqcseq 14065  ♯chash 14394  Basecbs 17301  +_gcplusg 17342  0_gc0g 17524   Σ_g cgsu 17525

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-seq 14066  df-gsum 17527

This theorem is used by:  gsumwsubmcl  18946  gsumccat  18950  gsumwmhm  18954  gsumwspan  18955  frmdgsum  18971  frmdup1  18973  mulgnn0gsum  19203  gsumwrev  19493  gsmsymgrfix  19555  gsmsymgreq  19559  psgnunilem2  19622  psgn0fv0  19638  psgnsn  19647  psgnprfval1  19649  gsumconst  20061  gsumle  20272  gsumfsum  21647  mplmonmul  22252  mplcoe1  22253  mplcoe5  22256  coe1fzgsumd  22529  evl1gsumd  22582  mdet0pr  22814  madugsum  22865  matunitlindflem1  22901  tmdgsum  24321  xrge0gsumle  25060  xrge0tsms  25061  jensen  27225  suppgsumssiun  33512  xrge0tsmsd  33513  gsumwun  33516  cyc3genpmlem  33591  gsumvsca1  33666  gsumvsca2  33667  elrgspnlem2  33683  elrgspnlem4  33685  domnprodn0  33718  domnprodeq0  33719  unitprodclb  33822  rprmdvdsprod  33944  1arithidom  33947  1arithufdlem3  33956  1arithufdlem4  33957  dfufd2lem  33959  deg1prod  33993  ply1coedeg  33999  psrgsum  34058  psrmonmul  34060  psrmonprod  34062  vieta  34090  zarcmplem  34391  esumnul  34558  esumsnf  34574  sitg0  34857  mrsub0  36095  evl1gprodd  42983  idomnnzgmulnz  42999  deg1gprod  43006  lincval0  49345