# 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 = ( ZMod ` G )`
Assertion zlmlmod
`|- ( G e. Abel <-> W e. LMod )`

### Proof

Step Hyp Ref Expression
1 zlmlmod.w
` |-  W = ( ZMod ` G )`
2 eqid
` |-  ( Base ` G ) = ( Base ` G )`
3 1 2 zlmbas
` |-  ( Base ` G ) = ( Base ` W )`
4 3 a1i
` |-  ( G e. Abel -> ( Base ` G ) = ( Base ` W ) )`
5 eqid
` |-  ( +g ` G ) = ( +g ` G )`
6 1 5 zlmplusg
` |-  ( +g ` G ) = ( +g ` W )`
7 6 a1i
` |-  ( G e. Abel -> ( +g ` G ) = ( +g ` W ) )`
8 1 zlmsca
` |-  ( G e. Abel -> ZZring = ( Scalar ` W ) )`
9 eqid
` |-  ( .g ` G ) = ( .g ` G )`
10 1 9 zlmvsca
` |-  ( .g ` G ) = ( .s ` W )`
11 10 a1i
` |-  ( G e. Abel -> ( .g ` G ) = ( .s ` W ) )`
12 zringbas
` |-  ZZ = ( Base ` ZZring )`
13 12 a1i
` |-  ( G e. Abel -> ZZ = ( Base ` ZZring ) )`
14 zringplusg
` |-  + = ( +g ` ZZring )`
15 14 a1i
` |-  ( G e. Abel -> + = ( +g ` ZZring ) )`
16 zringmulr
` |-  x. = ( .r ` ZZring )`
17 16 a1i
` |-  ( G e. Abel -> x. = ( .r ` ZZring ) )`
18 zring1
` |-  1 = ( 1r ` ZZring )`
19 18 a1i
` |-  ( G e. Abel -> 1 = ( 1r ` ZZring ) )`
20 zringring
` |-  ZZring e. Ring`
21 20 a1i
` |-  ( G e. Abel -> ZZring e. Ring )`
22 3 6 ablprop
` |-  ( G e. Abel <-> W e. Abel )`
23 ablgrp
` |-  ( W e. Abel -> W e. Grp )`
24 22 23 sylbi
` |-  ( G e. Abel -> W e. Grp )`
25 ablgrp
` |-  ( G e. Abel -> G e. Grp )`
26 2 9 mulgcl
` |-  ( ( G e. Grp /\ x e. ZZ /\ y e. ( Base ` G ) ) -> ( x ( .g ` G ) y ) e. ( Base ` G ) )`
27 25 26 syl3an1
` |-  ( ( G e. Abel /\ x e. ZZ /\ y e. ( Base ` G ) ) -> ( x ( .g ` G ) y ) e. ( Base ` G ) )`
28 2 9 5 mulgdi
` |-  ( ( G e. Abel /\ ( x e. ZZ /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ( .g ` G ) ( y ( +g ` G ) z ) ) = ( ( x ( .g ` G ) y ) ( +g ` G ) ( x ( .g ` G ) z ) ) )`
29 2 9 5 mulgdir
` |-  ( ( G e. Grp /\ ( x e. ZZ /\ y e. ZZ /\ z e. ( Base ` G ) ) ) -> ( ( x + y ) ( .g ` G ) z ) = ( ( x ( .g ` G ) z ) ( +g ` G ) ( y ( .g ` G ) z ) ) )`
30 25 29 sylan
` |-  ( ( G e. Abel /\ ( x e. ZZ /\ y e. ZZ /\ z e. ( Base ` G ) ) ) -> ( ( x + y ) ( .g ` G ) z ) = ( ( x ( .g ` G ) z ) ( +g ` G ) ( y ( .g ` G ) z ) ) )`
31 2 9 mulgass
` |-  ( ( G e. Grp /\ ( x e. ZZ /\ y e. ZZ /\ z e. ( Base ` G ) ) ) -> ( ( x x. y ) ( .g ` G ) z ) = ( x ( .g ` G ) ( y ( .g ` G ) z ) ) )`
32 25 31 sylan
` |-  ( ( G e. Abel /\ ( x e. ZZ /\ y e. ZZ /\ z e. ( Base ` G ) ) ) -> ( ( x x. y ) ( .g ` G ) z ) = ( x ( .g ` G ) ( y ( .g ` G ) z ) ) )`
33 2 9 mulg1
` |-  ( x e. ( Base ` G ) -> ( 1 ( .g ` G ) x ) = x )`
` |-  ( ( G e. Abel /\ x e. ( Base ` G ) ) -> ( 1 ( .g ` G ) x ) = x )`
` |-  ( G e. Abel -> W e. LMod )`
` |-  ( W e. LMod -> W e. Abel )`
` |-  ( W e. LMod -> G e. Abel )`
` |-  ( G e. Abel <-> W e. LMod )`