This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
Assertion zlmassa ( 𝐺 ∈ Ring ↔ 𝑊 ∈ AssAlg )

Proof

Step Hyp Ref Expression
1 zlmassa.w ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 1 2 zlmbas ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 )
4 3 a1i ⊢ ( 𝐺 ∈ Ring → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) )
5 1 zlmsca ⊢ ( 𝐺 ∈ Ring → ℤring = ( Scalar ‘ 𝑊 ) )
6 zringbas ⊢ ℤ = ( Base ‘ ℤring )
7 6 a1i ⊢ ( 𝐺 ∈ Ring → ℤ = ( Base ‘ ℤring ) )
8 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
9 1 8 zlmvsca ⊢ ( .g ‘ 𝐺 ) = ( ·𝑠 ‘ 𝑊 )
10 9 a1i ⊢ ( 𝐺 ∈ Ring → ( .g ‘ 𝐺 ) = ( ·𝑠 ‘ 𝑊 ) )
11 eqid ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
12 1 11 zlmmulr ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝑊 )
13 12 a1i ⊢ ( 𝐺 ∈ Ring → ( .r ‘ 𝐺 ) = ( .r ‘ 𝑊 ) )
14 ringabl ⊢ ( 𝐺 ∈ Ring → 𝐺 ∈ Abel )
15 1 zlmlmod ⊢ ( 𝐺 ∈ Abel ↔ 𝑊 ∈ LMod )
16 14 15 sylib ⊢ ( 𝐺 ∈ Ring → 𝑊 ∈ LMod )
17 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
18 1 17 zlmplusg ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 )
19 3 18 12 ringprop ⊢ ( 𝐺 ∈ Ring ↔ 𝑊 ∈ Ring )
20 19 biimpi ⊢ ( 𝐺 ∈ Ring → 𝑊 ∈ Ring )
21 2 8 11 mulgass2 ⊢ ( ( 𝐺 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( .g ‘ 𝐺 ) 𝑦 ) ( .r ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( .g ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑧 ) ) )
22 2 8 11 mulgass3 ⊢ ( ( 𝐺 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( .r ‘ 𝐺 ) ( 𝑥 ( .g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑥 ( .g ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑧 ) ) )
23 4 5 7 10 13 16 20 21 22 isassad ⊢ ( 𝐺 ∈ Ring → 𝑊 ∈ AssAlg )
24 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
25 24 19 sylibr ⊢ ( 𝑊 ∈ AssAlg → 𝐺 ∈ Ring )
26 23 25 impbii ⊢ ( 𝐺 ∈ Ring ↔ 𝑊 ∈ AssAlg )