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

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2		cnring	⊢ ℂfld ∈ Ring
3		rlmlmod	⊢ ( ℂfld ∈ Ring → ( ringLMod ‘ ℂfld ) ∈ LMod )
4	2 3	ax-mp	⊢ ( ringLMod ‘ ℂfld ) ∈ LMod
5	1 4	eqeltri	⊢ 𝐶 ∈ LMod