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 𝑊 = ( ℤ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 1 zlmsca ( 𝐺 ∈ Abel → ℤring = ( Scalar ‘ 𝑊 ) )
5 df-zring ring = ( ℂflds ℤ )
6 4 5 eqtr3di ( 𝐺 ∈ Abel → ( Scalar ‘ 𝑊 ) = ( ℂflds ℤ ) )
7 zsubrg ℤ ∈ ( SubRing ‘ ℂfld )
8 7 a1i ( 𝐺 ∈ Abel → ℤ ∈ ( SubRing ‘ ℂfld ) )
9 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10 9 isclmi ( ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂflds ℤ ) ∧ ℤ ∈ ( 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 )