# Metamath Proof Explorer

## Theorem gsummptfidmsplit

Description: Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019)

Ref Expression
Hypotheses gsummptfidmsplit.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsummptfidmsplit.p
gsummptfidmsplit.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsummptfidmsplit.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
gsummptfidmsplit.y ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {Y}\in {B}$
gsummptfidmsplit.i ${⊢}{\phi }\to {C}\cap {D}=\varnothing$
gsummptfidmsplit.u ${⊢}{\phi }\to {A}={C}\cup {D}$
Assertion gsummptfidmsplit

### Proof

Step Hyp Ref Expression
1 gsummptfidmsplit.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsummptfidmsplit.p
3 gsummptfidmsplit.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
4 gsummptfidmsplit.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
5 gsummptfidmsplit.y ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {Y}\in {B}$
6 gsummptfidmsplit.i ${⊢}{\phi }\to {C}\cap {D}=\varnothing$
7 gsummptfidmsplit.u ${⊢}{\phi }\to {A}={C}\cup {D}$
8 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
9 eqid ${⊢}\left({k}\in {A}⟼{Y}\right)=\left({k}\in {A}⟼{Y}\right)$
10 fvexd ${⊢}{\phi }\to {0}_{{G}}\in \mathrm{V}$
11 9 4 5 10 fsuppmptdm ${⊢}{\phi }\to {finSupp}_{{0}_{{G}}}\left(\left({k}\in {A}⟼{Y}\right)\right)$
12 1 8 2 3 4 5 11 6 7 gsumsplit2