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=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnrbas	$$⊢{\mathrm{Base}}_C=ℂ$$

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	$$⊢C=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
2		rlmbas	$$⊢{\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{Base}}_{\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)}$$
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4	1	fveq2i	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)}$$
5	2 3 4	3eqtr4ri	$$⊢{\mathrm{Base}}_C=ℂ$$