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 = ( ZMod ` G )
Assertion zlmclm
|- ( G e. Abel <-> W e. CMod )

Proof

Step Hyp Ref Expression
1 zlmclm.w
 |-  W = ( ZMod ` G )
2 1 zlmlmod
 |-  ( G e. Abel <-> W e. LMod )
3 2 biimpi
 |-  ( G e. Abel -> W e. LMod )
4 1 zlmsca
 |-  ( G e. Abel -> ZZring = ( Scalar ` W ) )
5 df-zring
 |-  ZZring = ( CCfld |`s ZZ )
6 4 5 eqtr3di
 |-  ( G e. Abel -> ( Scalar ` W ) = ( CCfld |`s ZZ ) )
7 zsubrg
 |-  ZZ e. ( SubRing ` CCfld )
8 7 a1i
 |-  ( G e. Abel -> ZZ e. ( SubRing ` CCfld ) )
9 eqid
 |-  ( Scalar ` W ) = ( Scalar ` W )
10 9 isclmi
 |-  ( ( W e. LMod /\ ( Scalar ` W ) = ( CCfld |`s ZZ ) /\ ZZ e. ( SubRing ` CCfld ) ) -> W e. CMod )
11 3 6 8 10 syl3anc
 |-  ( G e. Abel -> W e. CMod )
12 clmlmod
 |-  ( W e. CMod -> W e. LMod )
13 12 2 sylibr
 |-  ( W e. CMod -> G e. Abel )
14 11 13 impbii
 |-  ( G e. Abel <-> W e. CMod )