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