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 ⊢ Base G = Base G
3 1 2 zlmbas ⊢ Base G = Base W
4 3 a1i ⊢ G ∈ Abel → Base G = Base W
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 ∈ Base G → x ⋅ G y ∈ Base G
27 25 26 syl3an1 ⊢ G ∈ Abel ∧ x ∈ ℤ ∧ y ∈ Base G → x ⋅ G y ∈ Base G
28 2 9 5 mulgdi ⊢ G ∈ Abel ∧ x ∈ ℤ ∧ y ∈ Base G ∧ z ∈ Base G → x ⋅ G y + G z = x ⋅ G y + G x ⋅ G z
29 2 9 5 mulgdir ⊢ G ∈ Grp ∧ x ∈ ℤ ∧ y ∈ ℤ ∧ z ∈ Base G → x + y ⋅ G z = x ⋅ G z + G y ⋅ G z
30 25 29 sylan ⊢ G ∈ Abel ∧ x ∈ ℤ ∧ y ∈ ℤ ∧ z ∈ Base G → x + y ⋅ G z = x ⋅ G z + G y ⋅ G z
31 2 9 mulgass ⊢ G ∈ Grp ∧ x ∈ ℤ ∧ y ∈ ℤ ∧ z ∈ Base G → x ⁢ y ⋅ G z = x ⋅ G y ⋅ G z
32 25 31 sylan ⊢ G ∈ Abel ∧ x ∈ ℤ ∧ y ∈ ℤ ∧ z ∈ Base G → x ⁢ y ⋅ G z = x ⋅ G y ⋅ G z
33 2 9 mulg1 ⊢ x ∈ Base G → 1 ⋅ G x = x
34 33 adantl ⊢ G ∈ Abel ∧ x ∈ Base G → 1 ⋅ G x = 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