Theorem gsumsplit2

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumsplit2.b	|- B = ( Base ` G )
	gsumsplit2.z	|- .0. = ( 0g ` G )
	gsumsplit2.p	|- .+ = ( +g ` G )
	gsumsplit2.g	|- ( ph -> G e. CMnd )
	gsumsplit2.a	|- ( ph -> A e. V )
	gsumsplit2.f	|- ( ( ph /\ k e. A ) -> X e. B )
	gsumsplit2.w	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
	gsumsplit2.i	|- ( ph -> ( C i^i D ) = (/) )
	gsumsplit2.u	|- ( ph -> A = ( C u. D ) )
Assertion	gsumsplit2	|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. C |-> X ) ) .+ ( G gsum ( k e. D |-> X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumsplit2.b	|- B = ( Base ` G )
2		gsumsplit2.z	|- .0. = ( 0g ` G )
3		gsumsplit2.p	|- .+ = ( +g ` G )
4		gsumsplit2.g	|- ( ph -> G e. CMnd )
5		gsumsplit2.a	|- ( ph -> A e. V )
6		gsumsplit2.f	|- ( ( ph /\ k e. A ) -> X e. B )
7		gsumsplit2.w	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
8		gsumsplit2.i	|- ( ph -> ( C i^i D ) = (/) )
9		gsumsplit2.u	|- ( ph -> A = ( C u. D ) )
10	6	fmpttd	|- ( ph -> ( k e. A |-> X ) : A --> B )
11	1 2 3 4 5 10 7 8 9	gsumsplit	|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( ( k e. A |-> X ) |` C ) ) .+ ( G gsum ( ( k e. A |-> X ) |` D ) ) ) )
12		ssun1	|- C C_ ( C u. D )
13	12 9	sseqtrrid	|- ( ph -> C C_ A )
14	13	resmptd	|- ( ph -> ( ( k e. A |-> X ) |` C ) = ( k e. C |-> X ) )
15	14	oveq2d	|- ( ph -> ( G gsum ( ( k e. A |-> X ) |` C ) ) = ( G gsum ( k e. C |-> X ) ) )
16		ssun2	|- D C_ ( C u. D )
17	16 9	sseqtrrid	|- ( ph -> D C_ A )
18	17	resmptd	|- ( ph -> ( ( k e. A |-> X ) |` D ) = ( k e. D |-> X ) )
19	18	oveq2d	|- ( ph -> ( G gsum ( ( k e. A |-> X ) |` D ) ) = ( G gsum ( k e. D |-> X ) ) )
20	15 19	oveq12d	|- ( ph -> ( ( G gsum ( ( k e. A |-> X ) |` C ) ) .+ ( G gsum ( ( k e. A |-> X ) |` D ) ) ) = ( ( G gsum ( k e. C |-> X ) ) .+ ( G gsum ( k e. D |-> X ) ) ) )
21	11 20	eqtrd	|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. C |-> X ) ) .+ ( G gsum ( k e. D |-> X ) ) ) )