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

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
gsumvsmul.s ⊢ 𝑆 = ( Scalar ‘ 𝑅 )
gsumvsmul.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
gsumvsmul.z ⊢ 0 = ( 0g ‘ 𝑅 )
gsumvsmul.p ⊢ + = ( +g ‘ 𝑅 )
gsumvsmul.t ⊢ · = ( ·𝑠 ‘ 𝑅 )
gsumvsmul.r ⊢ ( 𝜑 → 𝑅 ∈ LMod )
gsumvsmul.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumvsmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
gsumvsmul.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
gsumvsmul.n ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) finSupp 0 )
Assertion gsumvsmul ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( 𝑋 · ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumvsmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 gsumvsmul.s ⊢ 𝑆 = ( Scalar ‘ 𝑅 )
3 gsumvsmul.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
4 gsumvsmul.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 gsumvsmul.p ⊢ + = ( +g ‘ 𝑅 )
6 gsumvsmul.t ⊢ · = ( ·𝑠 ‘ 𝑅 )
7 gsumvsmul.r ⊢ ( 𝜑 → 𝑅 ∈ LMod )
8 gsumvsmul.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
9 gsumvsmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
10 gsumvsmul.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
11 gsumvsmul.n ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) finSupp 0 )
12 lmodcmn ⊢ ( 𝑅 ∈ LMod → 𝑅 ∈ CMnd )
13 7 12 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
14 cmnmnd ⊢ ( 𝑅 ∈ CMnd → 𝑅 ∈ Mnd )
15 13 14 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
16 1 2 6 3 lmodvsghm ⊢ ( ( 𝑅 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 · 𝑦 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
17 7 9 16 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 · 𝑦 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
18 ghmmhm ⊢ ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 · 𝑦 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 · 𝑦 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
19 17 18 syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 · 𝑦 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
20 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
21 oveq2 ⊢ ( 𝑦 = ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) ) → ( 𝑋 · 𝑦 ) = ( 𝑋 · ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) ) ) )
22 1 4 13 15 8 19 10 11 20 21 gsummhm2 ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( 𝑋 · ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) ) ) )