# Metamath Proof Explorer

## Theorem gsummgp0

Description: If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019)

Ref Expression
Hypotheses gsummgp0.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
gsummgp0.0
gsummgp0.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
gsummgp0.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
gsummgp0.a ${⊢}\left({\phi }\wedge {n}\in {N}\right)\to {A}\in {\mathrm{Base}}_{{R}}$
gsummgp0.e ${⊢}\left({\phi }\wedge {n}={i}\right)\to {A}={B}$
gsummgp0.b
Assertion gsummgp0

### Proof

Step Hyp Ref Expression
1 gsummgp0.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
2 gsummgp0.0
3 gsummgp0.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
4 gsummgp0.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
5 gsummgp0.a ${⊢}\left({\phi }\wedge {n}\in {N}\right)\to {A}\in {\mathrm{Base}}_{{R}}$
6 gsummgp0.e ${⊢}\left({\phi }\wedge {n}={i}\right)\to {A}={B}$
7 gsummgp0.b
8 difsnid ${⊢}{i}\in {N}\to \left({N}\setminus \left\{{i}\right\}\right)\cup \left\{{i}\right\}={N}$
9 8 eqcomd ${⊢}{i}\in {N}\to {N}=\left({N}\setminus \left\{{i}\right\}\right)\cup \left\{{i}\right\}$
11 10 mpteq1d
12 11 oveq2d
13 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
14 1 13 mgpbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{G}}$
15 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
16 1 15 mgpplusg ${⊢}{\cdot }_{{R}}={+}_{{G}}$
17 1 crngmgp ${⊢}{R}\in \mathrm{CRing}\to {G}\in \mathrm{CMnd}$
18 3 17 syl ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
20 diffi ${⊢}{N}\in \mathrm{Fin}\to {N}\setminus \left\{{i}\right\}\in \mathrm{Fin}$
21 4 20 syl ${⊢}{\phi }\to {N}\setminus \left\{{i}\right\}\in \mathrm{Fin}$
23 simpl
24 eldifi ${⊢}{n}\in \left({N}\setminus \left\{{i}\right\}\right)\to {n}\in {N}$
25 23 24 5 syl2an
26 simprl
27 neldifsnd
28 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
29 3 28 syl ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
30 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
31 13 2 mndidcl
32 29 30 31 3syl
34 eleq1
36 33 35 mpbird
41 24 5 sylan2 ${⊢}\left({\phi }\wedge {n}\in \left({N}\setminus \left\{{i}\right\}\right)\right)\to {A}\in {\mathrm{Base}}_{{R}}$
42 41 ralrimiva ${⊢}{\phi }\to \forall {n}\in \left({N}\setminus \left\{{i}\right\}\right)\phantom{\rule{.4em}{0ex}}{A}\in {\mathrm{Base}}_{{R}}$
43 14 18 21 42 gsummptcl ${⊢}{\phi }\to \underset{{n}\in {N}\setminus \left\{{i}\right\}}{{\sum }_{{G}}}{A}\in {\mathrm{Base}}_{{R}}$