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 ˙ = 0 R
gsumvsmul.p + ˙ = + R
gsumvsmul.t · ˙ = R
gsumvsmul.r φ R LMod
gsumvsmul.a φ A V
gsumvsmul.x φ X K
gsumvsmul.y φ k A Y B
gsumvsmul.n φ finSupp 0 ˙ k A Y
Assertion gsumvsmul φ R k A X · ˙ Y = X · ˙ R k 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 ˙ = 0 R
5 gsumvsmul.p + ˙ = + R
6 gsumvsmul.t · ˙ = R
7 gsumvsmul.r φ R LMod
8 gsumvsmul.a φ A V
9 gsumvsmul.x φ X K
10 gsumvsmul.y φ k A Y B
11 gsumvsmul.n φ finSupp 0 ˙ k A Y
12 lmodcmn R LMod R CMnd
13 7 12 syl φ R CMnd
14 cmnmnd R CMnd R Mnd
15 13 14 syl φ R Mnd
16 1 2 6 3 lmodvsghm R LMod X K y B X · ˙ y R GrpHom R
17 7 9 16 syl2anc φ y B X · ˙ y R GrpHom R
18 ghmmhm y B X · ˙ y R GrpHom R y B X · ˙ y R MndHom R
19 17 18 syl φ y B X · ˙ y R MndHom R
20 oveq2 y = Y X · ˙ y = X · ˙ Y
21 oveq2 y = R k A Y X · ˙ y = X · ˙ R k A Y
22 1 4 13 15 8 19 10 11 20 21 gsummhm2 φ R k A X · ˙ Y = X · ˙ R k A Y