Theorem gsum0 18873

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 5260	. . . 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 18872	. 2 ⊢ (𝐺 ∈ V → (𝐺 Σg ∅) = 0 )
11		df-gsum 17613	. . . . 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 7554	. . . 4 ⊢ Rel dom Σg
13	12	ovprc1 7459	. . 3 ⊢ (¬ 𝐺 ∈ V → (𝐺 Σg ∅) = ∅)
14		fvprc 6877	. . . 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 1569  ∃wex 1811   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450  [wsbc 3738  ⦋csb 3846   ⊆ wss 3895   ∖ cdif 4045  ∅c0 4278  ifcif 4481  ^◡ccnv 5649  dom cdm 5650  ran crn 5651   “ cima 5653   ∘ ccom 5654  ℩cio 6492  ⟶wf 6534  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7420  1c1 11201  ℤ_≥cuz 12965  ...cfz 13639  seqcseq 14144  ♯chash 14474  Basecbs 17387  +_gcplusg 17428  0_gc0g 17610   Σ_g cgsu 17611

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-seq 14145  df-gsum 17613

This theorem is used by:  gsumwsubmcl  19033  gsumccat  19037  gsumwmhm  19041  gsumwspan  19042  frmdgsum  19058  frmdup1  19060  mulgnn0gsum  19290  gsumwrev  19580  gsmsymgrfix  19642  gsmsymgreq  19646  psgnunilem2  19709  psgn0fv0  19725  psgnsn  19734  psgnprfval1  19736  gsumconst  20148  gsumle  20359  gsumfsum  21740  mplmonmul  22345  mplcoe1  22346  mplcoe5  22349  coe1fzgsumd  22622  evl1gsumd  22675  mdet0pr  22907  madugsum  22958  matunitlindflem1  22994  tmdgsum  24414  xrge0gsumle  25153  xrge0tsms  25154  jensen  27316  suppgsumssiun  33633  xrge0tsmsd  33634  gsumwun  33637  cyc3genpmlem  33712  gsumvsca1  33787  gsumvsca2  33788  elrgspnlem2  33804  elrgspnlem4  33806  domnprodn0  33839  domnprodeq0  33840  unitprodclb  33944  rprmdvdsprod  34066  1arithidom  34069  1arithufdlem3  34078  1arithufdlem4  34079  dfufd2lem  34081  deg1prod  34115  ply1coedeg  34121  psrgsum  34180  psrmonmul  34182  psrmonprod  34184  vieta  34212  zarcmplem  34513  esumnul  34680  esumsnf  34696  sitg0  34978  mrsub0  36281  evl1gprodd  43168  idomnnzgmulnz  43184  deg1gprod  43191  lincval0  49527