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

Metamath Proof Explorer

Theorem gsummulc1OLD

Description: Obsolete version of gsummulc1 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses gsummulc1OLD.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
gsummulc1OLD.z ⊢ 0 = ( 0g ‘ 𝑅 )
gsummulc1OLD.p ⊢ + = ( +g ‘ 𝑅 )
gsummulc1OLD.t ⊢ · = ( .r ‘ 𝑅 )
gsummulc1OLD.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
gsummulc1OLD.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsummulc1OLD.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
gsummulc1OLD.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
gsummulc1OLD.n ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
Assertion gsummulc1OLD ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 gsummulc1OLD.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 gsummulc1OLD.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 gsummulc1OLD.p ⊢ + = ( +g ‘ 𝑅 )
4 gsummulc1OLD.t ⊢ · = ( .r ‘ 𝑅 )
5 gsummulc1OLD.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 gsummulc1OLD.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 gsummulc1OLD.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 gsummulc1OLD.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
9 gsummulc1OLD.n ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
10 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
11 5 10 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
12 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
13 5 12 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
14 1 4 ringrghm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
15 5 7 14 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
16 ghmmhm ⊢ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
17 15 16 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
18 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑌 ) = ( 𝑋 · 𝑌 ) )
19 oveq1 ⊢ ( 𝑥 = ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → ( 𝑥 · 𝑌 ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )
20 1 2 11 13 6 17 8 9 18 19 gsummhm2 ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )