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

Metamath Proof Explorer

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 )