This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ringLMod (ℂ_{fld})$
	Assertion	cnrlvec	$⊢ C \in LVec$

Proof

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