Metamath Proof Explorer


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 ) ) )