Metamath Proof Explorer


Theorem gsummulgz

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

Proof

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