Theorem gsumadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumadd.b	|- B = ( Base ` G )
	gsumadd.z	|- .0. = ( 0g ` G )
	gsumadd.p	|- .+ = ( +g ` G )
	gsumadd.g	|- ( ph -> G e. CMnd )
	gsumadd.a	|- ( ph -> A e. V )
	gsumadd.f	|- ( ph -> F : A --> B )
	gsumadd.h	|- ( ph -> H : A --> B )
	gsumadd.fn	|- ( ph -> F finSupp .0. )
	gsumadd.hn	|- ( ph -> H finSupp .0. )
Assertion	gsumadd	|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumadd.b	|- B = ( Base ` G )
2		gsumadd.z	|- .0. = ( 0g ` G )
3		gsumadd.p	|- .+ = ( +g ` G )
4		gsumadd.g	|- ( ph -> G e. CMnd )
5		gsumadd.a	|- ( ph -> A e. V )
6		gsumadd.f	|- ( ph -> F : A --> B )
7		gsumadd.h	|- ( ph -> H : A --> B )
8		gsumadd.fn	|- ( ph -> F finSupp .0. )
9		gsumadd.hn	|- ( ph -> H finSupp .0. )
10		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
11		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
12	4 11	syl	|- ( ph -> G e. Mnd )
13	1	submid	|- ( G e. Mnd -> B e. ( SubMnd ` G ) )
14	12 13	syl	|- ( ph -> B e. ( SubMnd ` G ) )
15		ssid	|- B C_ B
16	1 10	cntzcmn	|- ( ( G e. CMnd /\ B C_ B ) -> ( ( Cntz ` G ) ` B ) = B )
17	4 15 16	sylancl	|- ( ph -> ( ( Cntz ` G ) ` B ) = B )
18	15 17	sseqtrrid	|- ( ph -> B C_ ( ( Cntz ` G ) ` B ) )
19	1 2 3 10 12 5 8 9 14 18 6 7	gsumzadd	|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )