Metamath Proof Explorer

Theorem zlmassa

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

Ref Expression
Hypothesis zlmlmod.w ⊢ W = ℤMod ⁡ G
Assertion zlmassa ⊢ G ∈ Ring ↔ W ∈ AssAlg

Proof

Step Hyp Ref Expression
1 zlmlmod.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