# Metamath Proof Explorer

## Theorem gsumzunsnd

Description: Append an element to a finite group sum, more general version of gsumunsnd . (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses gsumzunsnd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumzunsnd.p
gsumzunsnd.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
gsumzunsnd.f ${⊢}{F}=\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)$
gsumzunsnd.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
gsumzunsnd.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
gsumzunsnd.c ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)$
gsumzunsnd.x ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
gsumzunsnd.m ${⊢}{\phi }\to {M}\in {V}$
gsumzunsnd.d ${⊢}{\phi }\to ¬{M}\in {A}$
gsumzunsnd.y ${⊢}{\phi }\to {Y}\in {B}$
gsumzunsnd.s ${⊢}\left({\phi }\wedge {k}={M}\right)\to {X}={Y}$
Assertion gsumzunsnd

### Proof

Step Hyp Ref Expression
1 gsumzunsnd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumzunsnd.p
3 gsumzunsnd.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
4 gsumzunsnd.f ${⊢}{F}=\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)$
5 gsumzunsnd.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
6 gsumzunsnd.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
7 gsumzunsnd.c ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)$
8 gsumzunsnd.x ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
9 gsumzunsnd.m ${⊢}{\phi }\to {M}\in {V}$
10 gsumzunsnd.d ${⊢}{\phi }\to ¬{M}\in {A}$
11 gsumzunsnd.y ${⊢}{\phi }\to {Y}\in {B}$
12 gsumzunsnd.s ${⊢}\left({\phi }\wedge {k}={M}\right)\to {X}={Y}$
13 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
14 snfi ${⊢}\left\{{M}\right\}\in \mathrm{Fin}$
15 unfi ${⊢}\left({A}\in \mathrm{Fin}\wedge \left\{{M}\right\}\in \mathrm{Fin}\right)\to {A}\cup \left\{{M}\right\}\in \mathrm{Fin}$
16 6 14 15 sylancl ${⊢}{\phi }\to {A}\cup \left\{{M}\right\}\in \mathrm{Fin}$
17 elun ${⊢}{k}\in \left({A}\cup \left\{{M}\right\}\right)↔\left({k}\in {A}\vee {k}\in \left\{{M}\right\}\right)$
18 elsni ${⊢}{k}\in \left\{{M}\right\}\to {k}={M}$
19 18 12 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left\{{M}\right\}\right)\to {X}={Y}$
20 11 adantr ${⊢}\left({\phi }\wedge {k}\in \left\{{M}\right\}\right)\to {Y}\in {B}$
21 19 20 eqeltrd ${⊢}\left({\phi }\wedge {k}\in \left\{{M}\right\}\right)\to {X}\in {B}$
22 8 21 jaodan ${⊢}\left({\phi }\wedge \left({k}\in {A}\vee {k}\in \left\{{M}\right\}\right)\right)\to {X}\in {B}$
23 17 22 sylan2b ${⊢}\left({\phi }\wedge {k}\in \left({A}\cup \left\{{M}\right\}\right)\right)\to {X}\in {B}$
24 23 4 fmptd ${⊢}{\phi }\to {F}:{A}\cup \left\{{M}\right\}⟶{B}$
25 8 expcom ${⊢}{k}\in {A}\to \left({\phi }\to {X}\in {B}\right)$
26 11 adantr ${⊢}\left({\phi }\wedge {k}={M}\right)\to {Y}\in {B}$
27 12 26 eqeltrd ${⊢}\left({\phi }\wedge {k}={M}\right)\to {X}\in {B}$
28 27 expcom ${⊢}{k}={M}\to \left({\phi }\to {X}\in {B}\right)$
29 18 28 syl ${⊢}{k}\in \left\{{M}\right\}\to \left({\phi }\to {X}\in {B}\right)$
30 25 29 jaoi ${⊢}\left({k}\in {A}\vee {k}\in \left\{{M}\right\}\right)\to \left({\phi }\to {X}\in {B}\right)$
31 17 30 sylbi ${⊢}{k}\in \left({A}\cup \left\{{M}\right\}\right)\to \left({\phi }\to {X}\in {B}\right)$
32 31 impcom ${⊢}\left({\phi }\wedge {k}\in \left({A}\cup \left\{{M}\right\}\right)\right)\to {X}\in {B}$
33 fvexd ${⊢}{\phi }\to {0}_{{G}}\in \mathrm{V}$
34 4 16 32 33 fsuppmptdm ${⊢}{\phi }\to {finSupp}_{{0}_{{G}}}\left({F}\right)$
35 disjsn ${⊢}{A}\cap \left\{{M}\right\}=\varnothing ↔¬{M}\in {A}$
36 10 35 sylibr ${⊢}{\phi }\to {A}\cap \left\{{M}\right\}=\varnothing$
37 eqidd ${⊢}{\phi }\to {A}\cup \left\{{M}\right\}={A}\cup \left\{{M}\right\}$
38 1 13 2 3 5 16 24 7 34 36 37 gsumzsplit
39 4 reseq1i ${⊢}{{F}↾}_{{A}}={\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)↾}_{{A}}$
40 ssun1 ${⊢}{A}\subseteq {A}\cup \left\{{M}\right\}$
41 resmpt ${⊢}{A}\subseteq {A}\cup \left\{{M}\right\}\to {\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)↾}_{{A}}=\left({k}\in {A}⟼{X}\right)$
42 40 41 mp1i ${⊢}{\phi }\to {\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)↾}_{{A}}=\left({k}\in {A}⟼{X}\right)$
43 39 42 syl5eq ${⊢}{\phi }\to {{F}↾}_{{A}}=\left({k}\in {A}⟼{X}\right)$
44 43 oveq2d ${⊢}{\phi }\to {\sum }_{{G}}\left({{F}↾}_{{A}}\right)=\underset{{k}\in {A}}{{\sum }_{{G}}}{X}$
45 4 reseq1i ${⊢}{{F}↾}_{\left\{{M}\right\}}={\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)↾}_{\left\{{M}\right\}}$
46 ssun2 ${⊢}\left\{{M}\right\}\subseteq {A}\cup \left\{{M}\right\}$
47 resmpt ${⊢}\left\{{M}\right\}\subseteq {A}\cup \left\{{M}\right\}\to {\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)↾}_{\left\{{M}\right\}}=\left({k}\in \left\{{M}\right\}⟼{X}\right)$
48 46 47 mp1i ${⊢}{\phi }\to {\left({k}\in \left({A}\cup \left\{{M}\right\}\right)⟼{X}\right)↾}_{\left\{{M}\right\}}=\left({k}\in \left\{{M}\right\}⟼{X}\right)$
49 45 48 syl5eq ${⊢}{\phi }\to {{F}↾}_{\left\{{M}\right\}}=\left({k}\in \left\{{M}\right\}⟼{X}\right)$
50 49 oveq2d ${⊢}{\phi }\to {\sum }_{{G}}\left({{F}↾}_{\left\{{M}\right\}}\right)=\underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{X}$
51 44 50 oveq12d
52 1 5 9 11 12 gsumsnd ${⊢}{\phi }\to \underset{{k}\in \left\{{M}\right\}}{{\sum }_{{G}}}{X}={Y}$
53 52 oveq2d
54 38 51 53 3eqtrd