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