# Metamath Proof Explorer

## Theorem zlmlmod

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

Ref Expression
Hypothesis zlmlmod.w 𝑊 = ( ℤMod ‘ 𝐺 )
Assertion zlmlmod ( 𝐺 ∈ Abel ↔ 𝑊 ∈ LMod )

### Proof

Step Hyp Ref Expression
1 zlmlmod.w 𝑊 = ( ℤMod ‘ 𝐺 )
2 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 1 2 zlmbas ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 )
4 3 a1i ( 𝐺 ∈ Abel → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) )
5 eqid ( +g𝐺 ) = ( +g𝐺 )
6 1 5 zlmplusg ( +g𝐺 ) = ( +g𝑊 )
7 6 a1i ( 𝐺 ∈ Abel → ( +g𝐺 ) = ( +g𝑊 ) )
8 1 zlmsca ( 𝐺 ∈ Abel → ℤring = ( Scalar ‘ 𝑊 ) )
9 eqid ( .g𝐺 ) = ( .g𝐺 )
10 1 9 zlmvsca ( .g𝐺 ) = ( ·𝑠𝑊 )
11 10 a1i ( 𝐺 ∈ Abel → ( .g𝐺 ) = ( ·𝑠𝑊 ) )
12 zringbas ℤ = ( Base ‘ ℤring )
13 12 a1i ( 𝐺 ∈ Abel → ℤ = ( Base ‘ ℤring ) )
14 zringplusg + = ( +g ‘ ℤring )
15 14 a1i ( 𝐺 ∈ Abel → + = ( +g ‘ ℤring ) )
16 zringmulr · = ( .r ‘ ℤring )
17 16 a1i ( 𝐺 ∈ Abel → · = ( .r ‘ ℤring ) )
18 zring1 1 = ( 1r ‘ ℤring )
19 18 a1i ( 𝐺 ∈ Abel → 1 = ( 1r ‘ ℤring ) )
20 zringring ring ∈ Ring
21 20 a1i ( 𝐺 ∈ Abel → ℤring ∈ Ring )
22 3 6 ablprop ( 𝐺 ∈ Abel ↔ 𝑊 ∈ Abel )
23 ablgrp ( 𝑊 ∈ Abel → 𝑊 ∈ Grp )
24 22 23 sylbi ( 𝐺 ∈ Abel → 𝑊 ∈ Grp )
25 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
26 2 9 mulgcl ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( .g𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
27 25 26 syl3an1 ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( .g𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
28 2 9 5 mulgdi ( ( 𝐺 ∈ Abel ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( .g𝐺 ) ( 𝑦 ( +g𝐺 ) 𝑧 ) ) = ( ( 𝑥 ( .g𝐺 ) 𝑦 ) ( +g𝐺 ) ( 𝑥 ( .g𝐺 ) 𝑧 ) ) )
29 2 9 5 mulgdir ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 + 𝑦 ) ( .g𝐺 ) 𝑧 ) = ( ( 𝑥 ( .g𝐺 ) 𝑧 ) ( +g𝐺 ) ( 𝑦 ( .g𝐺 ) 𝑧 ) ) )
30 25 29 sylan ( ( 𝐺 ∈ Abel ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 + 𝑦 ) ( .g𝐺 ) 𝑧 ) = ( ( 𝑥 ( .g𝐺 ) 𝑧 ) ( +g𝐺 ) ( 𝑦 ( .g𝐺 ) 𝑧 ) ) )
31 2 9 mulgass ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 · 𝑦 ) ( .g𝐺 ) 𝑧 ) = ( 𝑥 ( .g𝐺 ) ( 𝑦 ( .g𝐺 ) 𝑧 ) ) )
32 25 31 sylan ( ( 𝐺 ∈ Abel ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 · 𝑦 ) ( .g𝐺 ) 𝑧 ) = ( 𝑥 ( .g𝐺 ) ( 𝑦 ( .g𝐺 ) 𝑧 ) ) )
33 2 9 mulg1 ( 𝑥 ∈ ( Base ‘ 𝐺 ) → ( 1 ( .g𝐺 ) 𝑥 ) = 𝑥 )
34 33 adantl ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 1 ( .g𝐺 ) 𝑥 ) = 𝑥 )
35 4 7 8 11 13 15 17 19 21 24 27 28 30 32 34 islmodd ( 𝐺 ∈ Abel → 𝑊 ∈ LMod )
36 lmodabl ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
37 36 22 sylibr ( 𝑊 ∈ LMod → 𝐺 ∈ Abel )
38 35 37 impbii ( 𝐺 ∈ Abel ↔ 𝑊 ∈ LMod )