# Metamath Proof Explorer

## Theorem gsumsnd

Description: Group sum of a singleton, deduction form. (Contributed by Thierry Arnoux, 30-Jan-2017) (Proof shortened by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumsnd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumsnd.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
gsumsnd.m ${⊢}{\phi }\to {M}\in {V}$
gsumsnd.c ${⊢}{\phi }\to {C}\in {B}$
gsumsnd.s ${⊢}\left({\phi }\wedge {k}={M}\right)\to {A}={C}$
Assertion gsumsnd ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{A}={C}$

### Proof

Step Hyp Ref Expression
1 gsumsnd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumsnd.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
3 gsumsnd.m ${⊢}{\phi }\to {M}\in {V}$
4 gsumsnd.c ${⊢}{\phi }\to {C}\in {B}$
5 gsumsnd.s ${⊢}\left({\phi }\wedge {k}={M}\right)\to {A}={C}$
6 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
7 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{C}$
8 1 2 3 4 5 6 7 gsumsnfd ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{A}={C}$