Theorem clmsubrg

Description: The base set of the ring of scalars of a subcomplex module is the base set of a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	isclm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	isclm.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	clmsubrg	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )

Proof

Step	Hyp	Ref	Expression
1		isclm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		isclm.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	isclm	⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
4	3	simp3bi	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )