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 = Base G
gsummptfidmsplit.p + ˙ = + G
gsummptfidmsplit.g φ G CMnd
gsummptfidmsplit.a φ A Fin
gsummptfidmsplit.y φ k A Y B
gsummptfidmsplit.i φ C D =
gsummptfidmsplit.u φ A = C D
Assertion gsummptfidmsplit φ G k A Y = G k C Y + ˙ G k D Y

Proof

Step Hyp Ref Expression
1 gsummptfidmsplit.b B = Base G
2 gsummptfidmsplit.p + ˙ = + G
3 gsummptfidmsplit.g φ G CMnd
4 gsummptfidmsplit.a φ A Fin
5 gsummptfidmsplit.y φ k A Y B
6 gsummptfidmsplit.i φ C D =
7 gsummptfidmsplit.u φ A = C D
8 eqid 0 G = 0 G
9 eqid k A Y = k A Y
10 fvexd φ 0 G V
11 9 4 5 10 fsuppmptdm φ finSupp 0 G k A Y
12 1 8 2 3 4 5 11 6 7 gsumsplit2 φ G k A Y = G k C Y + ˙ G k D Y