Theorem cnrlmod

Description: The complex left module of complex numbers is a left module. 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	cnrlmod	$$⊢C\in \mathrm{LMod}$$

Proof

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