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 LVec

Proof

Step Hyp Ref Expression
1 cnrlmod.c 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 C LVec