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 = ℤMod G
Assertion zlmassa G Ring W AssAlg

Proof

Step Hyp Ref Expression
1 zlmassa.w W = ℤMod G
2 eqid Base G = Base G
3 1 2 zlmbas Base G = Base W
4 3 a1i G Ring Base G = Base W
5 1 zlmsca G Ring ring = Scalar W
6 zringbas = Base ring
7 6 a1i G Ring = Base ring
8 eqid G = G
9 1 8 zlmvsca G = W
10 9 a1i G Ring G = W
11 eqid G = G
12 1 11 zlmmulr G = W
13 12 a1i G Ring G = W
14 ringabl G Ring G Abel
15 1 zlmlmod G Abel W LMod
16 14 15 sylib G Ring W LMod
17 eqid + G = + G
18 1 17 zlmplusg + G = + W
19 3 18 12 ringprop G Ring W Ring
20 19 biimpi G Ring W Ring
21 zringcrng ring CRing
22 21 a1i G Ring ring CRing
23 2 8 11 mulgass2 G Ring x y Base G z Base G x G y G z = x G y G z
24 2 8 11 mulgass3 G Ring x y Base G z Base G y G x G z = x G y G z
25 4 5 7 10 13 16 20 22 23 24 isassad G Ring W AssAlg
26 assaring W AssAlg W Ring
27 26 19 sylibr W AssAlg G Ring
28 25 27 impbii G Ring W AssAlg