# Metamath Proof Explorer

## Theorem gsumsnfd

Description: Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Revised 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}$
gsumsnfd.p ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
gsumsnfd.c ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{C}$
Assertion gsumsnfd ${⊢}{\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 gsumsnfd.p ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
7 gsumsnfd.c ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{C}$
8 elsni ${⊢}{k}\in \left\{{M}\right\}\to {k}={M}$
9 8 5 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left\{{M}\right\}\right)\to {A}={C}$
10 6 9 mpteq2da ${⊢}{\phi }\to \left({k}\in \left\{{M}\right\}⟼{A}\right)=\left({k}\in \left\{{M}\right\}⟼{C}\right)$
11 10 oveq2d ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{A}=\underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{C}$
12 snfi ${⊢}\left\{{M}\right\}\in \mathrm{Fin}$
13 12 a1i ${⊢}{\phi }\to \left\{{M}\right\}\in \mathrm{Fin}$
14 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
15 7 1 14 gsumconstf ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left\{{M}\right\}\in \mathrm{Fin}\wedge {C}\in {B}\right)\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{C}=\left|\left\{{M}\right\}\right|{\cdot }_{{G}}{C}$
16 2 13 4 15 syl3anc ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{C}=\left|\left\{{M}\right\}\right|{\cdot }_{{G}}{C}$
17 11 16 eqtrd ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{A}=\left|\left\{{M}\right\}\right|{\cdot }_{{G}}{C}$
18 hashsng ${⊢}{M}\in {V}\to \left|\left\{{M}\right\}\right|=1$
19 3 18 syl ${⊢}{\phi }\to \left|\left\{{M}\right\}\right|=1$
20 19 oveq1d ${⊢}{\phi }\to \left|\left\{{M}\right\}\right|{\cdot }_{{G}}{C}=1{\cdot }_{{G}}{C}$
21 1 14 mulg1 ${⊢}{C}\in {B}\to 1{\cdot }_{{G}}{C}={C}$
22 4 21 syl ${⊢}{\phi }\to 1{\cdot }_{{G}}{C}={C}$
23 17 20 22 3eqtrd ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{A}={C}$