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 = ℤ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