Description: Integer multiple of a group sum. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by AV, 6-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsummulg.b | |- B = ( Base ` G ) |
|
gsummulg.z | |- .0. = ( 0g ` G ) |
||
gsummulg.t | |- .x. = ( .g ` G ) |
||
gsummulg.a | |- ( ph -> A e. V ) |
||
gsummulg.f | |- ( ( ph /\ k e. A ) -> X e. B ) |
||
gsummulg.w | |- ( ph -> ( k e. A |-> X ) finSupp .0. ) |
||
gsummulgz.g | |- ( ph -> G e. Abel ) |
||
gsummulgz.n | |- ( ph -> N e. ZZ ) |
||
Assertion | gsummulgz | |- ( ph -> ( G gsum ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsum ( k e. A |-> X ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsummulg.b | |- B = ( Base ` G ) |
|
2 | gsummulg.z | |- .0. = ( 0g ` G ) |
|
3 | gsummulg.t | |- .x. = ( .g ` G ) |
|
4 | gsummulg.a | |- ( ph -> A e. V ) |
|
5 | gsummulg.f | |- ( ( ph /\ k e. A ) -> X e. B ) |
|
6 | gsummulg.w | |- ( ph -> ( k e. A |-> X ) finSupp .0. ) |
|
7 | gsummulgz.g | |- ( ph -> G e. Abel ) |
|
8 | gsummulgz.n | |- ( ph -> N e. ZZ ) |
|
9 | ablcmn | |- ( G e. Abel -> G e. CMnd ) |
|
10 | 7 9 | syl | |- ( ph -> G e. CMnd ) |
11 | 7 | orcd | |- ( ph -> ( G e. Abel \/ N e. NN0 ) ) |
12 | 1 2 3 4 5 6 10 8 11 | gsummulglem | |- ( ph -> ( G gsum ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsum ( k e. A |-> X ) ) ) ) |