# Metamath Proof Explorer

## Theorem gsumunsnf

Description: Append an element to a finite group sum, 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 gsumunsnf.0 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{Y}$
gsumunsnf.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumunsnf.p
gsumunsnf.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsumunsnf.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
gsumunsnf.f ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
gsumunsnf.m ${⊢}{\phi }\to {M}\in {V}$
gsumunsnf.d ${⊢}{\phi }\to ¬{M}\in {A}$
gsumunsnf.y ${⊢}{\phi }\to {Y}\in {B}$
gsumunsnf.s ${⊢}{k}={M}\to {X}={Y}$
Assertion gsumunsnf

### Proof

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