Theorem gsumf1o

Description: Re-index a finite group sum using a bijection. (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 )
	gsumcl.w	|- ( ph -> F finSupp .0. )
	gsumf1o.h	|- ( ph -> H : C -1-1-onto-> A )
Assertion	gsumf1o	|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )

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		gsumcl.w	|- ( ph -> F finSupp .0. )
7		gsumf1o.h	|- ( ph -> H : C -1-1-onto-> A )
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	gsumzf1o	|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )