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 )