Metamath Proof Explorer

Theorem zlmclm

Description: The ZZ -module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015)

Ref Expression
Hypothesis zlmclm.w ⊢ W = ℤMod ⁡ G
Assertion zlmclm ⊢ G ∈ Abel ↔ W ∈ CMod

Proof

Step Hyp Ref Expression
1 zlmclm.w ⊢ W = ℤMod ⁡ G
2 1 zlmlmod ⊢ G ∈ Abel ↔ W ∈ LMod
3 2 biimpi ⊢ G ∈ Abel → W ∈ LMod
4 1 zlmsca ⊢ G ∈ Abel → ℤ ring = Scalar ⁡ W
5 df-zring ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ
6 4 5 eqtr3di ⊢ G ∈ Abel → Scalar ⁡ W = ℂ fld ↾ 𝑠 ℤ
7 zsubrg ⊢ ℤ ∈ SubRing ⁡ ℂ fld
8 7 a1i ⊢ G ∈ Abel → ℤ ∈ SubRing ⁡ ℂ fld
9 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
10 9 isclmi ⊢ W ∈ LMod ∧ Scalar ⁡ W = ℂ fld ↾ 𝑠 ℤ ∧ ℤ ∈ SubRing ⁡ ℂ fld → W ∈ CMod
11 3 6 8 10 syl3anc ⊢ G ∈ Abel → W ∈ CMod
12 clmlmod ⊢ W ∈ CMod → W ∈ LMod
13 12 2 sylibr ⊢ W ∈ CMod → G ∈ Abel
14 11 13 impbii ⊢ G ∈ Abel ↔ W ∈ CMod