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 )