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