# 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}={\mathrm{Base}}_{{R}}$
gsumvsmul.s ${⊢}{S}=\mathrm{Scalar}\left({R}\right)$
gsumvsmul.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
gsumvsmul.z
gsumvsmul.p
gsumvsmul.t
gsumvsmul.r ${⊢}{\phi }\to {R}\in \mathrm{LMod}$
gsumvsmul.a ${⊢}{\phi }\to {A}\in {V}$
gsumvsmul.x ${⊢}{\phi }\to {X}\in {K}$
gsumvsmul.y ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {Y}\in {B}$
gsumvsmul.n
Assertion gsumvsmul

### Proof

Step Hyp Ref Expression
1 gsumvsmul.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 gsumvsmul.s ${⊢}{S}=\mathrm{Scalar}\left({R}\right)$
3 gsumvsmul.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
4 gsumvsmul.z
5 gsumvsmul.p
6 gsumvsmul.t
7 gsumvsmul.r ${⊢}{\phi }\to {R}\in \mathrm{LMod}$
8 gsumvsmul.a ${⊢}{\phi }\to {A}\in {V}$
9 gsumvsmul.x ${⊢}{\phi }\to {X}\in {K}$
10 gsumvsmul.y ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {Y}\in {B}$
11 gsumvsmul.n
12 lmodcmn ${⊢}{R}\in \mathrm{LMod}\to {R}\in \mathrm{CMnd}$
13 7 12 syl ${⊢}{\phi }\to {R}\in \mathrm{CMnd}$
14 cmnmnd ${⊢}{R}\in \mathrm{CMnd}\to {R}\in \mathrm{Mnd}$
15 13 14 syl ${⊢}{\phi }\to {R}\in \mathrm{Mnd}$
16 1 2 6 3 lmodvsghm
17 7 9 16 syl2anc
18 ghmmhm
19 17 18 syl
20 oveq2
21 oveq2
22 1 4 13 15 8 19 10 11 20 21 gsummhm2