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	|- 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 ) )
	gsummptfidmsplitres.f	|- F = ( k e. A |-> Y )
Assertion	gsummptfidmsplitres	|- ( ph -> ( G gsum F ) = ( ( G gsum ( F |` C ) ) .+ ( G gsum ( F |` D ) ) ) )

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		gsummptfidmsplitres.f	|- F = ( k e. A |-> Y )
9		eqid	|- ( 0g ` G ) = ( 0g ` G )
10	5 8	fmptd	|- ( ph -> F : A --> B )
11		fvexd	|- ( ph -> ( 0g ` G ) e. _V )
12	8 4 5 11	fsuppmptdm	|- ( ph -> F finSupp ( 0g ` G ) )
13	1 9 2 3 4 10 12 6 7	gsumsplit	|- ( ph -> ( G gsum F ) = ( ( G gsum ( F |` C ) ) .+ ( G gsum ( F |` D ) ) ) )