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

Metamath Proof Explorer

Theorem clmsscn

Description: The scalar ring of a subcomplex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clm0.f ⊢ F = Scalar ⁡ W
clmsub.k ⊢ K = Base F
Assertion clmsscn ⊢ W ∈ CMod → K ⊆ ℂ

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ F = Scalar ⁡ W
2 clmsub.k ⊢ K = Base F
3 1 2 clmsubrg ⊢ W ∈ CMod → K ∈ SubRing ⁡ ℂ fld
4 cnfldbas ⊢ ℂ = Base ℂ fld
5 4 subrgss ⊢ K ∈ SubRing ⁡ ℂ fld → K ⊆ ℂ
6 3 5 syl ⊢ W ∈ CMod → K ⊆ ℂ