Metamath Proof Explorer


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 = ringLMod fld
Assertion cnrlmod C LMod

Proof

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