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	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion	cnrlvec	⊢ 𝐶 ∈ LVec

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2		cndrng	⊢ ℂfld ∈ DivRing
3		rlmlvec	⊢ ( ℂfld ∈ DivRing → ( ringLMod ‘ ℂfld ) ∈ LVec )
4	2 3	ax-mp	⊢ ( ringLMod ‘ ℂfld ) ∈ LVec
5	1 4	eqeltri	⊢ 𝐶 ∈ LVec