Theorem gsum0 18923

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 2763	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		gsum0.z	. . 3 ⊢ 0 = (0g‘𝐺)
3		eqid 2763	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
4		eqid 2763	. . 3 ⊢ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} = {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
5		id 23	. . 3 ⊢ (𝐺 ∈ V → 𝐺 ∈ V)
6		0ex 5267	. . . 4 ⊢ ∅ ∈ V
7	6	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅ ∈ V)
8		f0 6793	. . . 4 ⊢ ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
9	8	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ∅:∅⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)})
10	1, 2, 3, 4, 5, 7, 9	gsumval1 18922	. 2 ⊢ (𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
11		df-gsum 17663	. . . . 5 ⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))⟶1-1onto𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))))))
12	11	reldmmpo 7584	. . . 4 ⊢ Rel dom Σg
13	12	ovprc1 7490	. . 3 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = ∅)
14		fvprc 6908	. . . 4 ⊢ (¬ 𝐺 ∈ V → (0g‘𝐺) = ∅)
15	2, 14	eqtrid 2810	. . 3 ⊢ (¬ 𝐺 ∈ V → 0 = ∅)
16	13, 15	eqtr4d 2801	. 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 2147  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454  [wsbc 3742  ⦋csb 3851   ⊆ wss 3900   ∖ cdif 4048  ∅c0 4281  ifcif 4485  ^◡ccnv 5657  dom cdm 5658  ran crn 5659   “ cima 5661   ∘ ccom 5662  ℩cio 6518  ⟶wf 6562  ⟶1-1ontowf1o 6565  ‘cfv 6566  (class class class)co 7451  1c1 11240  ℤ_≥cuz 13005  ...cfz 13679  seqcseq 14184  ♯chash 14515  Basecbs 17431  +_gcplusg 17472  0_gc0g 17660   Σ_g cgsu 17661

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-seq 14185  df-gsum 17663

This theorem is used by:  gsumwsubmcl  19083  gsumccat  19087  gsumwmhm  19091  gsumwspan  19092  frmdgsum  19108  frmdup1  19110  mulgnn0gsum  19340  gsumwrev  19631  gsmsymgrfix  19693  gsmsymgreq  19697  psgnunilem2  19760  psgn0fv0  19776  psgnsn  19785  psgnprfval1  19787  gsumconst  20199  gsumle  20410  gsumfsum  21794  mplmonmul  22400  mplcoe1  22401  mplcoe5  22404  coe1fzgsumd  22677  evl1gsumd  22730  mdet0pr  22962  madugsum  23013  matunitlindflem1  23049  tmdgsum  24469  xrge0gsumle  25208  xrge0tsms  25209  jensen  27373  suppgsumssiun  33732  xrge0tsmsd  33733  gsumwun  33736  cyc3genpmlem  33811  gsumvsca1  33886  gsumvsca2  33887  elrgspnlem2  33903  elrgspnlem4  33905  domnprodn0  33938  domnprodeq0  33939  unitprodclb  34048  rprmdvdsprod  34170  1arithidom  34173  1arithufdlem3  34182  1arithufdlem4  34183  dfufd2lem  34185  deg1prod  34218  ply1coedeg  34224  psrgsum  34291  psrmonmul  34293  psrmonprod  34295  vieta  34323  zarcmplem  34624  esumnul  34791  esumsnf  34807  sitg0  35089  mrsub0  36489  evl1gprodd  43433  idomnnzgmulnz  43449  deg1gprod  43456  lincval0  49858