Metamath Proof Explorer

Theorem zlmassa

Description: The ZZ -module operation turns a ring into an associative algebra over ZZ . Also see zlmlmod . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypothesis zlmassa.w 
|- W = ( ZMod ` G )
Assertion zlmassa 
|- ( G e. Ring <-> W e. AssAlg )

Proof

Step Hyp Ref Expression
1 zlmassa.w 
 |-  W = ( ZMod ` G )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 1 2 zlmbas 
 |-  ( Base ` G ) = ( Base ` W )
4 3 a1i 
 |-  ( G e. Ring -> ( Base ` G ) = ( Base ` W ) )
5 1 zlmsca 
 |-  ( G e. Ring -> ZZring = ( Scalar ` W ) )
6 zringbas 
 |-  ZZ = ( Base ` ZZring )
7 6 a1i 
 |-  ( G e. Ring -> ZZ = ( Base ` ZZring ) )
8 eqid 
 |-  ( .g ` G ) = ( .g ` G )
9 1 8 zlmvsca 
 |-  ( .g ` G ) = ( .s ` W )
10 9 a1i 
 |-  ( G e. Ring -> ( .g ` G ) = ( .s ` W ) )
11 eqid 
 |-  ( .r ` G ) = ( .r ` G )
12 1 11 zlmmulr 
 |-  ( .r ` G ) = ( .r ` W )
13 12 a1i 
 |-  ( G e. Ring -> ( .r ` G ) = ( .r ` W ) )
14 ringabl 
 |-  ( G e. Ring -> G e. Abel )
15 1 zlmlmod 
 |-  ( G e. Abel <-> W e. LMod )
16 14 15 sylib 
 |-  ( G e. Ring -> W e. LMod )
17 eqid 
 |-  ( +g ` G ) = ( +g ` G )
18 1 17 zlmplusg 
 |-  ( +g ` G ) = ( +g ` W )
19 3 18 12 ringprop 
 |-  ( G e. Ring <-> W e. Ring )
20 19 biimpi 
 |-  ( G e. Ring -> W e. Ring )
21 2 8 11 mulgass2 
 |-  ( ( G e. Ring /\ ( x e. ZZ /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( .g ` G ) y ) ( .r ` G ) z ) = ( x ( .g ` G ) ( y ( .r ` G ) z ) ) )
22 2 8 11 mulgass3 
 |-  ( ( G e. Ring /\ ( x e. ZZ /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( y ( .r ` G ) ( x ( .g ` G ) z ) ) = ( x ( .g ` G ) ( y ( .r ` G ) z ) ) )
23 4 5 7 10 13 16 20 21 22 isassad 
 |-  ( G e. Ring -> W e. AssAlg )
24 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
25 24 19 sylibr 
 |-  ( W e. AssAlg -> G e. Ring )
26 23 25 impbii 
 |-  ( G e. Ring <-> W e. AssAlg )