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 ⊢W=ℤMod⁡G
Assertion zlmlmod ⊢G∈Abel↔W∈LMod

Proof

Step Hyp Ref Expression
1 zlmlmod.w ⊢W=ℤMod⁡G
2 eqid ⊢BaseG=BaseG
3 1 2 zlmbas ⊢BaseG=BaseW
4 3 a1i ⊢G∈Abel→BaseG=BaseW
5 eqid ⊢+G=+G
6 1 5 zlmplusg ⊢+G=+W
7 6 a1i ⊢G∈Abel→+G=+W
8 1 zlmsca ⊢G∈Abel→ℤring=Scalar⁡W
9 eqid ⊢⋅G=⋅G
10 1 9 zlmvsca ⊢⋅G=⋅W
11 10 a1i ⊢G∈Abel→⋅G=⋅W
12 zringbas ⊢ℤ=Baseℤring
13 12 a1i ⊢G∈Abel→ℤ=Baseℤring
14 zringplusg ⊢+=+ℤring
15 14 a1i ⊢G∈Abel→+=+ℤring
16 zringmulr ⊢×=⋅ℤring
17 16 a1i ⊢G∈Abel→×=⋅ℤring
18 zring1 ⊢1=1ℤring
19 18 a1i ⊢G∈Abel→1=1ℤring
20 zringring ⊢ℤring∈Ring
21 20 a1i ⊢G∈Abel→ℤring∈Ring
22 3 6 ablprop ⊢G∈Abel↔W∈Abel
23 ablgrp ⊢W∈Abel→W∈Grp
24 22 23 sylbi ⊢G∈Abel→W∈Grp
25 ablgrp ⊢G∈Abel→G∈Grp
26 2 9 mulgcl ⊢G∈Grp∧x∈ℤ∧y∈BaseG→x⋅Gy∈BaseG
27 25 26 syl3an1 ⊢G∈Abel∧x∈ℤ∧y∈BaseG→x⋅Gy∈BaseG
28 2 9 5 mulgdi ⊢G∈Abel∧x∈ℤ∧y∈BaseG∧z∈BaseG→x⋅Gy+Gz=x⋅Gy+Gx⋅Gz
29 2 9 5 mulgdir ⊢G∈Grp∧x∈ℤ∧y∈ℤ∧z∈BaseG→x+y⋅Gz=x⋅Gz+Gy⋅Gz
30 25 29 sylan ⊢G∈Abel∧x∈ℤ∧y∈ℤ∧z∈BaseG→x+y⋅Gz=x⋅Gz+Gy⋅Gz
31 2 9 mulgass ⊢G∈Grp∧x∈ℤ∧y∈ℤ∧z∈BaseG→x⁢y⋅Gz=x⋅Gy⋅Gz
32 25 31 sylan ⊢G∈Abel∧x∈ℤ∧y∈ℤ∧z∈BaseG→x⁢y⋅Gz=x⋅Gy⋅Gz
33 2 9 mulg1 ⊢x∈BaseG→1⋅Gx=x
34 33 adantl ⊢G∈Abel∧x∈BaseG→1⋅Gx=x
35 4 7 8 11 13 15 17 19 21 24 27 28 30 32 34 islmodd ⊢G∈Abel→W∈LMod
36 lmodabl ⊢W∈LMod→W∈Abel
37 36 22 sylibr ⊢W∈LMod→G∈Abel
38 35 37 impbii ⊢G∈Abel↔W∈LMod