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

Metamath Proof Explorer

Theorem clmzss

Description: The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmsub.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion clmzss ( 𝑊 ∈ ℂMod → ℤ ⊆ 𝐾 )

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 clmsub.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 1 2 clmsubrg ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
4 zsssubrg ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ℤ ⊆ 𝐾 )
5 3 4 syl ⊢ ( 𝑊 ∈ ℂMod → ℤ ⊆ 𝐾 )