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 ⊢ 𝑊 = ( ℤ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 = ( ℂfld ↾s ℤ )
6 4 5 eqtr3di ⊢ ( 𝐺 ∈ 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 )