# Metamath Proof Explorer

## Theorem gsumvsmul

Description: Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 , since every ring is a left module over itself. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by Mario Carneiro, 5-May-2015) (Revised by AV, 10-Jul-2019)

Ref Expression
Hypotheses gsumvsmul.b
`|- B = ( Base ` R )`
gsumvsmul.s
`|- S = ( Scalar ` R )`
gsumvsmul.k
`|- K = ( Base ` S )`
gsumvsmul.z
`|- .0. = ( 0g ` R )`
gsumvsmul.p
`|- .+ = ( +g ` R )`
gsumvsmul.t
`|- .x. = ( .s ` R )`
gsumvsmul.r
`|- ( ph -> R e. LMod )`
gsumvsmul.a
`|- ( ph -> A e. V )`
gsumvsmul.x
`|- ( ph -> X e. K )`
gsumvsmul.y
`|- ( ( ph /\ k e. A ) -> Y e. B )`
gsumvsmul.n
`|- ( ph -> ( k e. A |-> Y ) finSupp .0. )`
Assertion gsumvsmul
`|- ( ph -> ( R gsum ( k e. A |-> ( X .x. Y ) ) ) = ( X .x. ( R gsum ( k e. A |-> Y ) ) ) )`

### Proof

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