Theorem cnrbas

Description: The set of complex numbers is the base set of the complex left module of complex numbers. (Contributed by AV, 21-Sep-2021)

	Ref	Expression
Hypothesis	cnrlmod.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion	cnrbas	⊢ ( Base ‘ 𝐶 ) = ℂ

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2		rlmbas	⊢ ( Base ‘ ℂfld ) = ( Base ‘ ( ringLMod ‘ ℂfld ) )
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4	1	fveq2i	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( ringLMod ‘ ℂfld ) )
5	2 3 4	3eqtr4ri	⊢ ( Base ‘ 𝐶 ) = ℂ