# Metamath Proof Explorer

## Theorem gsumunsnd

Description: Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 2-Jan-2019) (Proof shortened by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumunsnd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumunsnd.p
gsumunsnd.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsumunsnd.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
gsumunsnd.f ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
gsumunsnd.m ${⊢}{\phi }\to {M}\in {V}$
gsumunsnd.d ${⊢}{\phi }\to ¬{M}\in {A}$
gsumunsnd.y ${⊢}{\phi }\to {Y}\in {B}$
gsumunsnd.s ${⊢}\left({\phi }\wedge {k}={M}\right)\to {X}={Y}$
Assertion gsumunsnd

### Proof

Step Hyp Ref Expression
1 gsumunsnd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumunsnd.p
3 gsumunsnd.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
4 gsumunsnd.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
5 gsumunsnd.f ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
6 gsumunsnd.m ${⊢}{\phi }\to {M}\in {V}$
7 gsumunsnd.d ${⊢}{\phi }\to ¬{M}\in {A}$
8 gsumunsnd.y ${⊢}{\phi }\to {Y}\in {B}$
9 gsumunsnd.s ${⊢}\left({\phi }\wedge {k}={M}\right)\to {X}={Y}$
10 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{Y}$
11 1 2 3 4 5 6 7 8 9 10 gsumunsnfd