# Metamath Proof Explorer

## Theorem zlmlmod

Description: The ZZ -module operation turns an arbitrary abelian group into a left module over ZZ . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypothesis zlmlmod.w ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
Assertion zlmlmod ${⊢}{G}\in \mathrm{Abel}↔{W}\in \mathrm{LMod}$

### Proof

Step Hyp Ref Expression
1 zlmlmod.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{Abel}\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{W}}$
5 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
6 1 5 zlmplusg ${⊢}{+}_{{G}}={+}_{{W}}$
7 6 a1i ${⊢}{G}\in \mathrm{Abel}\to {+}_{{G}}={+}_{{W}}$
8 1 zlmsca ${⊢}{G}\in \mathrm{Abel}\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left({W}\right)$
9 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
10 1 9 zlmvsca ${⊢}{\cdot }_{{G}}={\cdot }_{{W}}$
11 10 a1i ${⊢}{G}\in \mathrm{Abel}\to {\cdot }_{{G}}={\cdot }_{{W}}$
12 zringbas ${⊢}ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
13 12 a1i ${⊢}{G}\in \mathrm{Abel}\to ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
14 zringplusg ${⊢}+={+}_{{ℤ}_{\mathrm{ring}}}$
15 14 a1i ${⊢}{G}\in \mathrm{Abel}\to +={+}_{{ℤ}_{\mathrm{ring}}}$
16 zringmulr ${⊢}×={\cdot }_{{ℤ}_{\mathrm{ring}}}$
17 16 a1i ${⊢}{G}\in \mathrm{Abel}\to ×={\cdot }_{{ℤ}_{\mathrm{ring}}}$
18 zring1 ${⊢}1={1}_{{ℤ}_{\mathrm{ring}}}$
19 18 a1i ${⊢}{G}\in \mathrm{Abel}\to 1={1}_{{ℤ}_{\mathrm{ring}}}$
20 zringring ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
21 20 a1i ${⊢}{G}\in \mathrm{Abel}\to {ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
22 3 6 ablprop ${⊢}{G}\in \mathrm{Abel}↔{W}\in \mathrm{Abel}$
23 ablgrp ${⊢}{W}\in \mathrm{Abel}\to {W}\in \mathrm{Grp}$
24 22 23 sylbi ${⊢}{G}\in \mathrm{Abel}\to {W}\in \mathrm{Grp}$
25 ablgrp ${⊢}{G}\in \mathrm{Abel}\to {G}\in \mathrm{Grp}$
26 2 9 mulgcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {x}\in ℤ\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {x}{\cdot }_{{G}}{y}\in {\mathrm{Base}}_{{G}}$
27 25 26 syl3an1 ${⊢}\left({G}\in \mathrm{Abel}\wedge {x}\in ℤ\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {x}{\cdot }_{{G}}{y}\in {\mathrm{Base}}_{{G}}$
28 2 9 5 mulgdi ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({x}\in ℤ\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to {x}{\cdot }_{{G}}\left({y}{+}_{{G}}{z}\right)=\left({x}{\cdot }_{{G}}{y}\right){+}_{{G}}\left({x}{\cdot }_{{G}}{z}\right)$
29 2 9 5 mulgdir ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({x}\in ℤ\wedge {y}\in ℤ\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}+{y}\right){\cdot }_{{G}}{z}=\left({x}{\cdot }_{{G}}{z}\right){+}_{{G}}\left({y}{\cdot }_{{G}}{z}\right)$
30 25 29 sylan ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({x}\in ℤ\wedge {y}\in ℤ\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}+{y}\right){\cdot }_{{G}}{z}=\left({x}{\cdot }_{{G}}{z}\right){+}_{{G}}\left({y}{\cdot }_{{G}}{z}\right)$
31 2 9 mulgass ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({x}\in ℤ\wedge {y}\in ℤ\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to {x}{y}{\cdot }_{{G}}{z}={x}{\cdot }_{{G}}\left({y}{\cdot }_{{G}}{z}\right)$
32 25 31 sylan ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({x}\in ℤ\wedge {y}\in ℤ\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to {x}{y}{\cdot }_{{G}}{z}={x}{\cdot }_{{G}}\left({y}{\cdot }_{{G}}{z}\right)$
33 2 9 mulg1 ${⊢}{x}\in {\mathrm{Base}}_{{G}}\to 1{\cdot }_{{G}}{x}={x}$
34 33 adantl ${⊢}\left({G}\in \mathrm{Abel}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to 1{\cdot }_{{G}}{x}={x}$
35 4 7 8 11 13 15 17 19 21 24 27 28 30 32 34 islmodd ${⊢}{G}\in \mathrm{Abel}\to {W}\in \mathrm{LMod}$
36 lmodabl ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Abel}$
37 36 22 sylibr ${⊢}{W}\in \mathrm{LMod}\to {G}\in \mathrm{Abel}$
38 35 37 impbii ${⊢}{G}\in \mathrm{Abel}↔{W}\in \mathrm{LMod}$