Theorem gsum0 18763

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 2765	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		gsum0.z	. . 3 ⊢ 0 = (0g‘𝐺)
3		eqid 2765	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
4		eqid 2765	. . 3 ⊢ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} = {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
5		id 23	. . 3 ⊢ (𝐺 ∈ V → 𝐺 ∈ V)
6		0ex 5272	. . . 4 ⊢ ∅ ∈ V
7	6	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅ ∈ V)
8		f0 6763	. . . 4 ⊢ ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
9	8	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)})
10	1, 2, 3, 4, 5, 7, 9	gsumval1 18762	. 2 ⊢ (𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
11		df-gsum 17512	. . . . 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 7550	. . . 4 ⊢ Rel dom Σg
13	12	ovprc1 7455	. . 3 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = ∅)
14		fvprc 6877	. . . 4 ⊢ (¬ 𝐺 ∈ V → (0g‘𝐺) = ∅)
15	2, 14	eqtrid 2812	. . 3 ⊢ (¬ 𝐺 ∈ V → 0 = ∅)
16	13, 15	eqtr4d 2803	. 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 2146  ∀wral 3081  ∃wrex 3091  {crab 3418  Vcvv 3457  [wsbc 3746  ⦋csb 3854   ∖ cdif 3903   ⊆ wss 3906  ∅c0 4286  ifcif 4489  ^◡ccnv 5662  dom cdm 5663  ran crn 5664   “ cima 5666   ∘ ccom 5667  ℩cio 6494  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7416  1c1 11112  ℤ_≥cuz 12873  ...cfz 13546  seqcseq 14050  ♯chash 14379  Basecbs 17286  +_gcplusg 17327  0_gc0g 17509   Σ_g cgsu 17510

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-seq 14051  df-gsum 17512

This theorem is used by:  gsumwsubmcl  18919  gsumccat  18923  gsumwmhm  18927  gsumwspan  18928  frmdgsum  18944  frmdup1  18946  mulgnn0gsum  19169  gsumwrev  19459  gsmsymgrfix  19521  gsmsymgreq  19525  psgnunilem2  19588  psgn0fv0  19604  psgnsn  19613  psgnprfval1  19615  gsumconst  20027  gsumle  20238  gsumfsum  21613  mplmonmul  22216  mplcoe1  22217  mplcoe5  22220  coe1fzgsumd  22493  evl1gsumd  22546  mdet0pr  22778  madugsum  22829  tmdgsum  24281  xrge0gsumle  25020  xrge0tsms  25021  jensen  27182  suppgsumssiun  33415  xrge0tsmsd  33416  gsumwun  33419  cyc3genpmlem  33494  gsumvsca1  33569  gsumvsca2  33570  elrgspnlem2  33586  elrgspnlem4  33588  domnprodn0  33621  domnprodeq0  33622  unitprodclb  33725  rprmdvdsprod  33847  1arithidom  33850  1arithufdlem3  33859  1arithufdlem4  33860  dfufd2lem  33862  deg1prod  33896  ply1coedeg  33902  psrgsum  33961  psrmonmul  33963  psrmonprod  33965  vieta  33993  zarcmplem  34294  esumnul  34461  esumsnf  34477  sitg0  34760  mrsub0  36021  matunitlindflem1  38300  evl1gprodd  42917  idomnnzgmulnz  42933  deg1gprod  42940  lincval0  49228