Metamath Proof Explorer


Theorem gsummptfidmsplitres

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

Ref Expression
Hypotheses gsummptfidmsplit.b 𝐵 = ( Base ‘ 𝐺 )
gsummptfidmsplit.p + = ( +g𝐺 )
gsummptfidmsplit.g ( 𝜑𝐺 ∈ CMnd )
gsummptfidmsplit.a ( 𝜑𝐴 ∈ Fin )
gsummptfidmsplit.y ( ( 𝜑𝑘𝐴 ) → 𝑌𝐵 )
gsummptfidmsplit.i ( 𝜑 → ( 𝐶𝐷 ) = ∅ )
gsummptfidmsplit.u ( 𝜑𝐴 = ( 𝐶𝐷 ) )
gsummptfidmsplitres.f 𝐹 = ( 𝑘𝐴𝑌 )
Assertion gsummptfidmsplitres ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹𝐶 ) ) + ( 𝐺 Σg ( 𝐹𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfidmsplit.b 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfidmsplit.p + = ( +g𝐺 )
3 gsummptfidmsplit.g ( 𝜑𝐺 ∈ CMnd )
4 gsummptfidmsplit.a ( 𝜑𝐴 ∈ Fin )
5 gsummptfidmsplit.y ( ( 𝜑𝑘𝐴 ) → 𝑌𝐵 )
6 gsummptfidmsplit.i ( 𝜑 → ( 𝐶𝐷 ) = ∅ )
7 gsummptfidmsplit.u ( 𝜑𝐴 = ( 𝐶𝐷 ) )
8 gsummptfidmsplitres.f 𝐹 = ( 𝑘𝐴𝑌 )
9 eqid ( 0g𝐺 ) = ( 0g𝐺 )
10 5 8 fmptd ( 𝜑𝐹 : 𝐴𝐵 )
11 fvexd ( 𝜑 → ( 0g𝐺 ) ∈ V )
12 8 4 5 11 fsuppmptdm ( 𝜑𝐹 finSupp ( 0g𝐺 ) )
13 1 9 2 3 4 10 12 6 7 gsumsplit ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹𝐶 ) ) + ( 𝐺 Σg ( 𝐹𝐷 ) ) ) )