Theorem gsumres

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

	Ref	Expression
Hypotheses	gsumcl.b	|- B = ( Base ` G )
	gsumcl.z	|- .0. = ( 0g ` G )
	gsumcl.g	|- ( ph -> G e. CMnd )
	gsumcl.a	|- ( ph -> A e. V )
	gsumcl.f	|- ( ph -> F : A --> B )
	gsumres.s	|- ( ph -> ( F supp .0. ) C_ W )
	gsumres.w	|- ( ph -> F finSupp .0. )
Assertion	gsumres	|- ( ph -> ( G gsum ( F |` W ) ) = ( G gsum F ) )

Proof

Step	Hyp	Ref	Expression
1		gsumcl.b	|- B = ( Base ` G )
2		gsumcl.z	|- .0. = ( 0g ` G )
3		gsumcl.g	|- ( ph -> G e. CMnd )
4		gsumcl.a	|- ( ph -> A e. V )
5		gsumcl.f	|- ( ph -> F : A --> B )
6		gsumres.s	|- ( ph -> ( F supp .0. ) C_ W )
7		gsumres.w	|- ( ph -> F finSupp .0. )
8		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
9		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
10	3 9	syl	|- ( ph -> G e. Mnd )
11	1 8 3 5	cntzcmnf	|- ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
12	1 2 8 10 4 5 11 6 7	gsumzres	|- ( ph -> ( G gsum ( F |` W ) ) = ( G gsum F ) )