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

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 )