# Metamath Proof Explorer

## Theorem gsumsnf

Description: Group sum of a singleton, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumsnf.c ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{C}$
gsumsnf.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumsnf.s ${⊢}{k}={M}\to {A}={C}$
Assertion gsumsnf ${⊢}\left({G}\in \mathrm{Mnd}\wedge {M}\in {V}\wedge {C}\in {B}\right)\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{A}={C}$

### Proof

Step Hyp Ref Expression
1 gsumsnf.c ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{C}$
2 gsumsnf.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 gsumsnf.s ${⊢}{k}={M}\to {A}={C}$
4 simp1 ${⊢}\left({G}\in \mathrm{Mnd}\wedge {M}\in {V}\wedge {C}\in {B}\right)\to {G}\in \mathrm{Mnd}$
5 simp2 ${⊢}\left({G}\in \mathrm{Mnd}\wedge {M}\in {V}\wedge {C}\in {B}\right)\to {M}\in {V}$
6 simp3 ${⊢}\left({G}\in \mathrm{Mnd}\wedge {M}\in {V}\wedge {C}\in {B}\right)\to {C}\in {B}$
7 3 adantl ${⊢}\left(\left({G}\in \mathrm{Mnd}\wedge {M}\in {V}\wedge {C}\in {B}\right)\wedge {k}={M}\right)\to {A}={C}$
8 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{G}\in \mathrm{Mnd}$
9 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{M}\in {V}$
10 1 nfel1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{C}\in {B}$
11 8 9 10 nf3an ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({G}\in \mathrm{Mnd}\wedge {M}\in {V}\wedge {C}\in {B}\right)$
12 2 4 5 6 7 11 1 gsumsnfd ${⊢}\left({G}\in \mathrm{Mnd}\wedge {M}\in {V}\wedge {C}\in {B}\right)\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{A}={C}$