This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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