This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric subcomplex vector spaces Subcomplex vector spaces 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 ⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion
cnrlvec ⊢ 𝐶 ∈ LVec
Proof
Step
Hyp
Ref
Expression
1
cnrlmod.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 ⊢ 𝐶 ∈ LVec