# Metamath Proof Explorer

## Theorem zlmassa

Description: The ZZ -module operation turns a ring into an associative algebra over ZZ . Also see zlmlmod . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypothesis zlmassa.w ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
Assertion zlmassa ${⊢}{G}\in \mathrm{Ring}↔{W}\in \mathrm{AssAlg}$

### Proof

Step Hyp Ref Expression
1 zlmassa.w ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
2 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
3 1 2 zlmbas ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{W}}$
4 3 a1i ${⊢}{G}\in \mathrm{Ring}\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{W}}$
5 1 zlmsca ${⊢}{G}\in \mathrm{Ring}\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left({W}\right)$
6 zringbas ${⊢}ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
7 6 a1i ${⊢}{G}\in \mathrm{Ring}\to ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
8 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
9 1 8 zlmvsca ${⊢}{\cdot }_{{G}}={\cdot }_{{W}}$
10 9 a1i ${⊢}{G}\in \mathrm{Ring}\to {\cdot }_{{G}}={\cdot }_{{W}}$
11 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
12 1 11 zlmmulr ${⊢}{\cdot }_{{G}}={\cdot }_{{W}}$
13 12 a1i ${⊢}{G}\in \mathrm{Ring}\to {\cdot }_{{G}}={\cdot }_{{W}}$
14 ringabl ${⊢}{G}\in \mathrm{Ring}\to {G}\in \mathrm{Abel}$
15 1 zlmlmod ${⊢}{G}\in \mathrm{Abel}↔{W}\in \mathrm{LMod}$
16 14 15 sylib ${⊢}{G}\in \mathrm{Ring}\to {W}\in \mathrm{LMod}$
17 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
18 1 17 zlmplusg ${⊢}{+}_{{G}}={+}_{{W}}$
19 3 18 12 ringprop ${⊢}{G}\in \mathrm{Ring}↔{W}\in \mathrm{Ring}$
20 19 biimpi ${⊢}{G}\in \mathrm{Ring}\to {W}\in \mathrm{Ring}$
21 zringcrng ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{CRing}$
22 21 a1i ${⊢}{G}\in \mathrm{Ring}\to {ℤ}_{\mathrm{ring}}\in \mathrm{CRing}$
23 2 8 11 mulgass2 ${⊢}\left({G}\in \mathrm{Ring}\wedge \left({x}\in ℤ\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}{\cdot }_{{G}}{y}\right){\cdot }_{{G}}{z}={x}{\cdot }_{{G}}\left({y}{\cdot }_{{G}}{z}\right)$
24 2 8 11 mulgass3 ${⊢}\left({G}\in \mathrm{Ring}\wedge \left({x}\in ℤ\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to {y}{\cdot }_{{G}}\left({x}{\cdot }_{{G}}{z}\right)={x}{\cdot }_{{G}}\left({y}{\cdot }_{{G}}{z}\right)$
25 4 5 7 10 13 16 20 22 23 24 isassad ${⊢}{G}\in \mathrm{Ring}\to {W}\in \mathrm{AssAlg}$
26 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
27 26 19 sylibr ${⊢}{W}\in \mathrm{AssAlg}\to {G}\in \mathrm{Ring}$
28 25 27 impbii ${⊢}{G}\in \mathrm{Ring}↔{W}\in \mathrm{AssAlg}$