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 ` CCfld ) |
|
| Assertion | cnrlmod | |- C e. LMod |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnrlmod.c | |- C = ( ringLMod ` CCfld ) |
|
| 2 | cnring | |- CCfld e. Ring |
|
| 3 | rlmlmod | |- ( CCfld e. Ring -> ( ringLMod ` CCfld ) e. LMod ) |
|
| 4 | 2 3 | ax-mp | |- ( ringLMod ` CCfld ) e. LMod |
| 5 | 1 4 | eqeltri | |- C e. LMod |