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