Theorem gsumz 17602

Description: Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.)

Hypothesis

Ref	Expression
gsumz.z	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
gsumz	⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )

Distinct variable groups:   𝐴,𝑘   𝑘,𝐺   𝑘,𝑉

Allowed substitution hint:   0 (𝑘)

Proof of Theorem gsumz

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2774	. 2 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		gsumz.z	. 2 ⊢ 0 = (0g‘𝐺)
3		eqid 2774	. 2 ⊢ (+g‘𝐺) = (+g‘𝐺)
4		eqid 2774	. 2 ⊢ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} = {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)}
5		simpl 469	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → 𝐺 ∈ Mnd)
6		simpr 472	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
7	2	fvexi 6360	. . . . . 6 ⊢ 0 ∈ V
8	7	snid 4358	. . . . 5 ⊢ 0 ∈ { 0 }
9	1, 2, 3, 4	gsumvallem2 17600	. . . . 5 ⊢ (𝐺 ∈ Mnd → {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)} = { 0 })
10	8, 9	syl5eleqr 2860	. . . 4 ⊢ (𝐺 ∈ Mnd → 0 ∈ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)})
11	10	ad2antrr 706	. . 3 ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) ∧ 𝑘 ∈ 𝐴) → 0 ∈ {𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)})
12	11	fmpttd 6545	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝑘 ∈ 𝐴 ↦ 0 ):𝐴⟶{𝑥 ∈ (Base‘𝐺) ∣ ∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦)})
13	1, 2, 3, 4, 5, 6, 12	gsumval1 17505	1 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1634   ∈ wcel 2148  ∀wral 3064  {crab 3068  {csn 4326   ↦ cmpt 4876  ‘cfv 6042  (class class class)co 6812  Basecbs 16084  +_gcplusg 16169  0_gc0g 16328   Σ_g cgsu 16329  Mndcmnd 17522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-seq 13031  df-0g 16330  df-gsum 16331  df-mgm 17470  df-sgrp 17512  df-mnd 17523

This theorem is referenced by:  gsumval3  18535  gsumzres  18537  gsumzcl2  18538  gsumzf1o  18540  gsumzaddlem  18548  gsumzmhm  18564  gsumzoppg  18571  gsum2d  18598  dprdfeq0  18649  dprddisj2  18666  mplsubrglem  19674  evlslem1  19750  coe1tmmul2  19881  coe1tmmul  19882  cply1mul  19899  gsummoncoe1  19909  dmatmul  20541  smadiadetlem1a  20708  cpmatmcllem  20763  mp2pm2mplem4  20854  chfacfscmulgsum  20905  chfacfpmmulgsum  20909  tsms0  22185  tgptsmscls  22193  tdeglem4  24061  mdegmullem  24079  dchrptlem3  25233  gsummptres  30141  esum0  30468  ply1mulgsumlem2  42727  lincvalsc0  42762  linc0scn0  42764