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

Metamath Proof Explorer

Theorem gsummulc1

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019) Remove unused hypothesis. (Revised by SN, 7-Mar-2025)

Ref Expression
Hypotheses gsummulc1.b 
|- B = ( Base ` R )
gsummulc1.z 
|- .0. = ( 0g ` R )
gsummulc1.t 
|- .x. = ( .r ` R )
gsummulc1.r 
|- ( ph -> R e. Ring )
gsummulc1.a 
|- ( ph -> A e. V )
gsummulc1.y 
|- ( ph -> Y e. B )
gsummulc1.x 
|- ( ( ph /\ k e. A ) -> X e. B )
gsummulc1.n 
|- ( ph -> ( k e. A |-> X ) finSupp .0. )
Assertion gsummulc1 
|- ( ph -> ( R gsum ( k e. A |-> ( X .x. Y ) ) ) = ( ( R gsum ( k e. A |-> X ) ) .x. Y ) )

Proof

Step Hyp Ref Expression
1 gsummulc1.b 
 |-  B = ( Base ` R )
2 gsummulc1.z 
 |-  .0. = ( 0g ` R )
3 gsummulc1.t 
 |-  .x. = ( .r ` R )
4 gsummulc1.r 
 |-  ( ph -> R e. Ring )
5 gsummulc1.a 
 |-  ( ph -> A e. V )
6 gsummulc1.y 
 |-  ( ph -> Y e. B )
7 gsummulc1.x 
 |-  ( ( ph /\ k e. A ) -> X e. B )
8 gsummulc1.n 
 |-  ( ph -> ( k e. A |-> X ) finSupp .0. )
9 4 ringcmnd 
 |-  ( ph -> R e. CMnd )
10 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
11 4 10 syl 
 |-  ( ph -> R e. Mnd )
12 1 3 ringrghm 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( x e. B |-> ( x .x. Y ) ) e. ( R GrpHom R ) )
13 4 6 12 syl2anc 
 |-  ( ph -> ( x e. B |-> ( x .x. Y ) ) e. ( R GrpHom R ) )
14 ghmmhm 
 |-  ( ( x e. B |-> ( x .x. Y ) ) e. ( R GrpHom R ) -> ( x e. B |-> ( x .x. Y ) ) e. ( R MndHom R ) )
15 13 14 syl 
 |-  ( ph -> ( x e. B |-> ( x .x. Y ) ) e. ( R MndHom R ) )
16 oveq1 
 |-  ( x = X -> ( x .x. Y ) = ( X .x. Y ) )
17 oveq1 
 |-  ( x = ( R gsum ( k e. A |-> X ) ) -> ( x .x. Y ) = ( ( R gsum ( k e. A |-> X ) ) .x. Y ) )
18 1 2 9 11 5 15 7 8 16 17 gsummhm2 
 |-  ( ph -> ( R gsum ( k e. A |-> ( X .x. Y ) ) ) = ( ( R gsum ( k e. A |-> X ) ) .x. Y ) )