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 )
34 33 adantl 
 |-  ( ( G e. Abel /\ x e. ( Base ` G ) ) -> ( 1 ( .g ` G ) x ) = x )
35 4 7 8 11 13 15 17 19 21 24 27 28 30 32 34 islmodd 
 |-  ( G e. Abel -> W e. LMod )
36 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
37 36 22 sylibr 
 |-  ( W e. LMod -> G e. Abel )
38 35 37 impbii 
 |-  ( G e. Abel <-> W e. LMod )