# Metamath Proof Explorer

## Theorem gsumunsnfd

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 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}$
gsumunsnfd.0 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{Y}$
Assertion gsumunsnfd

### 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 gsumunsnfd.0 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{Y}$
11 snfi ${⊢}\left\{{M}\right\}\in \mathrm{Fin}$
12 unfi ${⊢}\left({A}\in \mathrm{Fin}\wedge \left\{{M}\right\}\in \mathrm{Fin}\right)\to {A}\cup \left\{{M}\right\}\in \mathrm{Fin}$
13 4 11 12 sylancl ${⊢}{\phi }\to {A}\cup \left\{{M}\right\}\in \mathrm{Fin}$
14 elun ${⊢}{k}\in \left({A}\cup \left\{{M}\right\}\right)↔\left({k}\in {A}\vee {k}\in \left\{{M}\right\}\right)$
15 elsni ${⊢}{k}\in \left\{{M}\right\}\to {k}={M}$
16 15 9 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left\{{M}\right\}\right)\to {X}={Y}$
17 8 adantr ${⊢}\left({\phi }\wedge {k}\in \left\{{M}\right\}\right)\to {Y}\in {B}$
18 16 17 eqeltrd ${⊢}\left({\phi }\wedge {k}\in \left\{{M}\right\}\right)\to {X}\in {B}$
19 5 18 jaodan ${⊢}\left({\phi }\wedge \left({k}\in {A}\vee {k}\in \left\{{M}\right\}\right)\right)\to {X}\in {B}$
20 14 19 sylan2b ${⊢}\left({\phi }\wedge {k}\in \left({A}\cup \left\{{M}\right\}\right)\right)\to {X}\in {B}$
21 disjsn ${⊢}{A}\cap \left\{{M}\right\}=\varnothing ↔¬{M}\in {A}$
22 7 21 sylibr ${⊢}{\phi }\to {A}\cap \left\{{M}\right\}=\varnothing$
23 eqidd ${⊢}{\phi }\to {A}\cup \left\{{M}\right\}={A}\cup \left\{{M}\right\}$
24 1 2 3 13 20 22 23 gsummptfidmsplit
25 cmnmnd ${⊢}{G}\in \mathrm{CMnd}\to {G}\in \mathrm{Mnd}$
26 3 25 syl ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
27 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
28 1 26 6 8 9 27 10 gsumsnfd ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{X}={Y}$
29 28 oveq2d
30 24 29 eqtrd