Theorem zlmlmod

Description: The ZZ -module operation turns an arbitrary abelian group into a left module over ZZ . Also see zlmassa . (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypothesis	zlmlmod.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
Assertion	zlmlmod	⊢ ( 𝐺 ∈ Abel ↔ 𝑊 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		zlmlmod.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3	1 2	zlmbas	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 )
4	3	a1i	⊢ ( 𝐺 ∈ Abel → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) )
5		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6	1 5	zlmplusg	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 )
7	6	a1i	⊢ ( 𝐺 ∈ Abel → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 ) )
8	1	zlmsca	⊢ ( 𝐺 ∈ Abel → ℤring = ( Scalar ‘ 𝑊 ) )
9		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
10	1 9	zlmvsca	⊢ ( .g ‘ 𝐺 ) = ( ·𝑠 ‘ 𝑊 )
11	10	a1i	⊢ ( 𝐺 ∈ Abel → ( .g ‘ 𝐺 ) = ( ·𝑠 ‘ 𝑊 ) )
12		zringbas	⊢ ℤ = ( Base ‘ ℤring )
13	12	a1i	⊢ ( 𝐺 ∈ Abel → ℤ = ( Base ‘ ℤring ) )
14		zringplusg	⊢ + = ( +g ‘ ℤring )
15	14	a1i	⊢ ( 𝐺 ∈ Abel → + = ( +g ‘ ℤring ) )
16		zringmulr	⊢ · = ( .r ‘ ℤring )
17	16	a1i	⊢ ( 𝐺 ∈ Abel → · = ( .r ‘ ℤring ) )
18		zring1	⊢ 1 = ( 1r ‘ ℤring )
19	18	a1i	⊢ ( 𝐺 ∈ Abel → 1 = ( 1r ‘ ℤring ) )
20		zringring	⊢ ℤring ∈ Ring
21	20	a1i	⊢ ( 𝐺 ∈ Abel → ℤring ∈ Ring )
22	3 6	ablprop	⊢ ( 𝐺 ∈ Abel ↔ 𝑊 ∈ Abel )
23		ablgrp	⊢ ( 𝑊 ∈ Abel → 𝑊 ∈ Grp )
24	22 23	sylbi	⊢ ( 𝐺 ∈ Abel → 𝑊 ∈ Grp )
25		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
26	2 9	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( .g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
27	25 26	syl3an1	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( .g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
28	2 9 5	mulgdi	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( .g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝑥 ( .g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑥 ( .g ‘ 𝐺 ) 𝑧 ) ) )
29	2 9 5	mulgdir	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 + 𝑦 ) ( .g ‘ 𝐺 ) 𝑧 ) = ( ( 𝑥 ( .g ‘ 𝐺 ) 𝑧 ) ( +g ‘ 𝐺 ) ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) ) )
30	25 29	sylan	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 + 𝑦 ) ( .g ‘ 𝐺 ) 𝑧 ) = ( ( 𝑥 ( .g ‘ 𝐺 ) 𝑧 ) ( +g ‘ 𝐺 ) ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) ) )
31	2 9	mulgass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 · 𝑦 ) ( .g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( .g ‘ 𝐺 ) ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) ) )
32	25 31	sylan	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 · 𝑦 ) ( .g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( .g ‘ 𝐺 ) ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) ) )
33	2 9	mulg1	⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
34	33	adantl	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
35	4 7 8 11 13 15 17 19 21 24 27 28 30 32 34	islmodd	⊢ ( 𝐺 ∈ Abel → 𝑊 ∈ LMod )
36		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
37	36 22	sylibr	⊢ ( 𝑊 ∈ LMod → 𝐺 ∈ Abel )
38	35 37	impbii	⊢ ( 𝐺 ∈ Abel ↔ 𝑊 ∈ LMod )