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

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 ⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion cnrlmod 𝐶 ∈ LMod

Proof

Step Hyp Ref Expression
1 cnrlmod.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 ⊢ 𝐶 ∈ LMod