Theorem cnrlvec

Description: The complex left module of complex numbers is a left vector space. The vector operation is + , and the scalar product is x. . (Contributed by AV, 21-Sep-2021)

	Ref	Expression
Hypothesis	cnrlmod.c	$$⊢C=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnrlvec	$$⊢C\in \mathrm{LVec}$$

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	$$⊢C=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
3		rlmlvec	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}\to \mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{LVec}$$
4	2 3	ax-mp	$$⊢\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{LVec}$$
5	1 4	eqeltri	$$⊢C\in \mathrm{LVec}$$