Theorem gsumsplit

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

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

Proof

Step	Hyp	Ref	Expression
1		gsumsplit.b	|- B = ( Base ` G )
2		gsumsplit.z	|- .0. = ( 0g ` G )
3		gsumsplit.p	|- .+ = ( +g ` G )
4		gsumsplit.g	|- ( ph -> G e. CMnd )
5		gsumsplit.a	|- ( ph -> A e. V )
6		gsumsplit.f	|- ( ph -> F : A --> B )
7		gsumsplit.w	|- ( ph -> F finSupp .0. )
8		gsumsplit.i	|- ( ph -> ( C i^i D ) = (/) )
9		gsumsplit.u	|- ( ph -> A = ( C u. D ) )
10		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
11		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
12	4 11	syl	|- ( ph -> G e. Mnd )
13	1 10 4 6	cntzcmnf	|- ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
14	1 2 3 10 12 5 6 13 7 8 9	gsumzsplit	|- ( ph -> ( G gsum F ) = ( ( G gsum ( F |` C ) ) .+ ( G gsum ( F |` D ) ) ) )