Metamath Proof Explorer

Theorem cnrnvc

Description: The module of complex numbers (as a module over itself) is a normed vector space over itself. The vector operation is + , and the scalar product is x. , and the norm function is abs . (Contributed by AV, 9-Oct-2021)

Ref Expression
Hypothesis cnrnvc.c ⊢ C = ringLMod ⁡ ℂ fld
Assertion cnrnvc ⊢ C ∈ NrmVec

Proof

Step Hyp Ref Expression
1 cnrnvc.c ⊢ C = ringLMod ⁡ ℂ fld
2 cnnrg ⊢ ℂ fld ∈ NrmRing
3 cndrng ⊢ ℂ fld ∈ DivRing
4 rlmnvc ⊢ ℂ fld ∈ NrmRing ∧ ℂ fld ∈ DivRing → ringLMod ⁡ ℂ fld ∈ NrmVec
5 1 4 eqeltrid ⊢ ℂ fld ∈ NrmRing ∧ ℂ fld ∈ DivRing → C ∈ NrmVec
6 2 3 5 mp2an ⊢ C ∈ NrmVec