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 e. CMod -> K C_ CC )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	|- F = ( Scalar ` W )
2		clmsub.k	|- K = ( Base ` F )
3	1 2	clmsubrg	|- ( W e. CMod -> K e. ( SubRing ` CCfld ) )
4		cnfldbas	|- CC = ( Base ` CCfld )
5	4	subrgss	|- ( K e. ( SubRing ` CCfld ) -> K C_ CC )
6	3 5	syl	|- ( W e. CMod -> K C_ CC )