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	|- C = ( ringLMod ` CCfld )
Assertion	cnrbas	|- ( Base ` C ) = CC

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	|- C = ( ringLMod ` CCfld )
2		rlmbas	|- ( Base ` CCfld ) = ( Base ` ( ringLMod ` CCfld ) )
3		cnfldbas	|- CC = ( Base ` CCfld )
4	1	fveq2i	|- ( Base ` C ) = ( Base ` ( ringLMod ` CCfld ) )
5	2 3 4	3eqtr4ri	|- ( Base ` C ) = CC