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 2 8 11 mulgass2 G Ring x y Base G z Base G x G y G z = x G y G z
22 2 8 11 mulgass3 G Ring x y Base G z Base G y G x G z = x G y G z
23 4 5 7 10 13 16 20 21 22 isassad G Ring W AssAlg
24 assaring W AssAlg W Ring
25 24 19 sylibr W AssAlg G Ring
26 23 25 impbii G Ring W AssAlg