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	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
Assertion	zlmclm	⊢ ( 𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod )

Proof

Step	Hyp	Ref	Expression
1		zlmclm.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2	1	zlmlmod	⊢ ( 𝐺 ∈ Abel ↔ 𝑊 ∈ LMod )
3	2	biimpi	⊢ ( 𝐺 ∈ Abel → 𝑊 ∈ LMod )
4		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
5	1	zlmsca	⊢ ( 𝐺 ∈ Abel → ℤring = ( Scalar ‘ 𝑊 ) )
6	4 5	syl5reqr	⊢ ( 𝐺 ∈ Abel → ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ℤ ) )
7		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
8	7	a1i	⊢ ( 𝐺 ∈ Abel → ℤ ∈ ( SubRing ‘ ℂfld ) )
9		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10	9	isclmi	⊢ ( ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ℤ ) ∧ ℤ ∈ ( SubRing ‘ ℂfld ) ) → 𝑊 ∈ ℂMod )
11	3 6 8 10	syl3anc	⊢ ( 𝐺 ∈ Abel → 𝑊 ∈ ℂMod )
12		clmlmod	⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
13	12 2	sylibr	⊢ ( 𝑊 ∈ ℂMod → 𝐺 ∈ Abel )
14	11 13	impbii	⊢ ( 𝐺 ∈ Abel ↔ 𝑊 ∈ ℂMod )