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