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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	clmsub.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	clmsscn	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )

Proof

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