Database
BASIC TOPOLOGY
Metric subcomplex vector spaces
Subcomplex vector spaces
cnrlvec
Metamath Proof Explorer
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 ⁡ ℂ fld
Assertion
cnrlvec
⊢ C ∈ LVec
Proof
Step
Hyp
Ref
Expression
1
cnrlmod.c
⊢ 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
⊢ C ∈ LVec