Metamath Proof Explorer


Theorem gsummulgc2

Description: A finite group sum multiplied by a constant. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses gsummulgc1.b
|- B = ( Base ` M )
gsummulgc1.t
|- .x. = ( .g ` M )
gsummulgc1.r
|- ( ph -> M e. Grp )
gsummulgc1.a
|- ( ph -> A e. Fin )
gsummulgc1.y
|- ( ph -> Y e. B )
gsummulgc1.x
|- ( ( ph /\ k e. A ) -> X e. ZZ )
Assertion gsummulgc2
|- ( ph -> ( M gsum ( k e. A |-> ( X .x. Y ) ) ) = ( sum_ k e. A X .x. Y ) )

Proof

Step Hyp Ref Expression
1 gsummulgc1.b
 |-  B = ( Base ` M )
2 gsummulgc1.t
 |-  .x. = ( .g ` M )
3 gsummulgc1.r
 |-  ( ph -> M e. Grp )
4 gsummulgc1.a
 |-  ( ph -> A e. Fin )
5 gsummulgc1.y
 |-  ( ph -> Y e. B )
6 gsummulgc1.x
 |-  ( ( ph /\ k e. A ) -> X e. ZZ )
7 zringbas
 |-  ZZ = ( Base ` ZZring )
8 zring0
 |-  0 = ( 0g ` ZZring )
9 zringring
 |-  ZZring e. Ring
10 ringcmn
 |-  ( ZZring e. Ring -> ZZring e. CMnd )
11 9 10 mp1i
 |-  ( ph -> ZZring e. CMnd )
12 3 grpmndd
 |-  ( ph -> M e. Mnd )
13 eqid
 |-  ( x e. ZZ |-> ( x .x. Y ) ) = ( x e. ZZ |-> ( x .x. Y ) )
14 2 13 1 mulgghm2
 |-  ( ( M e. Grp /\ Y e. B ) -> ( x e. ZZ |-> ( x .x. Y ) ) e. ( ZZring GrpHom M ) )
15 3 5 14 syl2anc
 |-  ( ph -> ( x e. ZZ |-> ( x .x. Y ) ) e. ( ZZring GrpHom M ) )
16 ghmmhm
 |-  ( ( x e. ZZ |-> ( x .x. Y ) ) e. ( ZZring GrpHom M ) -> ( x e. ZZ |-> ( x .x. Y ) ) e. ( ZZring MndHom M ) )
17 15 16 syl
 |-  ( ph -> ( x e. ZZ |-> ( x .x. Y ) ) e. ( ZZring MndHom M ) )
18 eqid
 |-  ( k e. A |-> X ) = ( k e. A |-> X )
19 0zd
 |-  ( ph -> 0 e. ZZ )
20 18 4 6 19 fsuppmptdm
 |-  ( ph -> ( k e. A |-> X ) finSupp 0 )
21 oveq1
 |-  ( x = X -> ( x .x. Y ) = ( X .x. Y ) )
22 oveq1
 |-  ( x = ( ZZring gsum ( k e. A |-> X ) ) -> ( x .x. Y ) = ( ( ZZring gsum ( k e. A |-> X ) ) .x. Y ) )
23 7 8 11 12 4 17 6 20 21 22 gsummhm2
 |-  ( ph -> ( M gsum ( k e. A |-> ( X .x. Y ) ) ) = ( ( ZZring gsum ( k e. A |-> X ) ) .x. Y ) )
24 4 6 gsumzrsum
 |-  ( ph -> ( ZZring gsum ( k e. A |-> X ) ) = sum_ k e. A X )
25 24 oveq1d
 |-  ( ph -> ( ( ZZring gsum ( k e. A |-> X ) ) .x. Y ) = ( sum_ k e. A X .x. Y ) )
26 23 25 eqtrd
 |-  ( ph -> ( M gsum ( k e. A |-> ( X .x. Y ) ) ) = ( sum_ k e. A X .x. Y ) )