Theorem clmsca

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

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

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	simp2bi	⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )