Theorem gsumreidx

Description: Re-index a finite group sum using a bijection. Corresponds to the first equation in Lang p. 5 with M = 1 . (Contributed by AV, 26-Dec-2023)

	Ref	Expression
Hypotheses	gsumreidx.b	|- B = ( Base ` G )
	gsumreidx.z	|- .0. = ( 0g ` G )
	gsumreidx.g	|- ( ph -> G e. CMnd )
	gsumreidx.f	|- ( ph -> F : ( M ... N ) --> B )
	gsumreidx.h	|- ( ph -> H : ( M ... N ) -1-1-onto-> ( M ... N ) )
Assertion	gsumreidx	|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumreidx.b	|- B = ( Base ` G )
2		gsumreidx.z	|- .0. = ( 0g ` G )
3		gsumreidx.g	|- ( ph -> G e. CMnd )
4		gsumreidx.f	|- ( ph -> F : ( M ... N ) --> B )
5		gsumreidx.h	|- ( ph -> H : ( M ... N ) -1-1-onto-> ( M ... N ) )
6		ovexd	|- ( ph -> ( M ... N ) e. _V )
7		fzfid	|- ( ph -> ( M ... N ) e. Fin )
8	2	fvexi	|- .0. e. _V
9	8	a1i	|- ( ph -> .0. e. _V )
10	4 7 9	fdmfifsupp	|- ( ph -> F finSupp .0. )
11	1 2 3 6 4 10 5	gsumf1o	|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )