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 ` G )
	gsummptfidmsplit.g	|- ( ph -> G e. CMnd )
	gsummptfidmsplit.a	|- ( ph -> A e. Fin )
	gsummptfidmsplit.y	|- ( ( ph /\ k e. A ) -> Y e. B )
	gsummptfidmsplit.i	|- ( ph -> ( C i^i D ) = (/) )
	gsummptfidmsplit.u	|- ( ph -> A = ( C u. D ) )
Assertion	gsummptfidmsplit	|- ( ph -> ( G gsum ( k e. A |-> Y ) ) = ( ( G gsum ( k e. C |-> Y ) ) .+ ( G gsum ( k e. D |-> Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmsplit.b	|- B = ( Base ` G )
2		gsummptfidmsplit.p	|- .+ = ( +g ` G )
3		gsummptfidmsplit.g	|- ( ph -> G e. CMnd )
4		gsummptfidmsplit.a	|- ( ph -> A e. Fin )
5		gsummptfidmsplit.y	|- ( ( ph /\ k e. A ) -> Y e. B )
6		gsummptfidmsplit.i	|- ( ph -> ( C i^i D ) = (/) )
7		gsummptfidmsplit.u	|- ( ph -> A = ( C u. D ) )
8		eqid	|- ( 0g ` G ) = ( 0g ` G )
9		eqid	|- ( k e. A |-> Y ) = ( k e. A |-> Y )
10		fvexd	|- ( ph -> ( 0g ` G ) e. _V )
11	9 4 5 10	fsuppmptdm	|- ( ph -> ( k e. A |-> Y ) finSupp ( 0g ` G ) )
12	1 8 2 3 4 5 11 6 7	gsumsplit2	|- ( ph -> ( G gsum ( k e. A |-> Y ) ) = ( ( G gsum ( k e. C |-> Y ) ) .+ ( G gsum ( k e. D |-> Y ) ) ) )