Metamath Proof Explorer


Theorem gsummulc2

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019)

Ref Expression
Hypotheses gsummulc1.b
|- B = ( Base ` R )
gsummulc1.z
|- .0. = ( 0g ` R )
gsummulc1.p
|- .+ = ( +g ` 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 gsummulc2
|- ( ph -> ( R gsum ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) )

Proof

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