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

Metamath Proof Explorer

Theorem gsumvsmul1

Description: Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 , since every ring is a left module over itself. (Contributed by Thierry Arnoux, 12-Jun-2023)

Ref Expression
Hypotheses gsumvsmul1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
gsumvsmul1.s ⊢ 𝑆 = ( Scalar ‘ 𝑅 )
gsumvsmul1.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
gsumvsmul1.z ⊢ 0 = ( 0g ‘ 𝑆 )
gsumvsmul1.t ⊢ · = ( ·𝑠 ‘ 𝑅 )
gsumvsmul1.r ⊢ ( 𝜑 → 𝑅 ∈ LMod )
gsumvsmul1.1 ⊢ ( 𝜑 → 𝑆 ∈ CMnd )
gsumvsmul1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumvsmul1.x ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
gsumvsmul1.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐾 )
gsumvsmul1.n ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
Assertion gsumvsmul1 ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )

Proof

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