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 ` CCfld ) |
|
| Assertion | cnrlvec | |- C e. LVec |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnrlmod.c | |- C = ( ringLMod ` CCfld ) |
|
| 2 | cndrng | |- CCfld e. DivRing |
|
| 3 | rlmlvec | |- ( CCfld e. DivRing -> ( ringLMod ` CCfld ) e. LVec ) |
|
| 4 | 2 3 | ax-mp | |- ( ringLMod ` CCfld ) e. LVec |
| 5 | 1 4 | eqeltri | |- C e. LVec |