Metamath Proof Explorer

Theorem rlmnvc

Description: The ring module over a normed division ring is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion rlmnvc ⊢ R ∈ NrmRing ∧ R ∈ DivRing → ringLMod ⁡ R ∈ NrmVec

Proof

Step Hyp Ref Expression
1 rlmnlm ⊢ R ∈ NrmRing → ringLMod ⁡ R ∈ NrmMod
2 rlmlvec ⊢ R ∈ DivRing → ringLMod ⁡ R ∈ LVec
3 isnvc ⊢ ringLMod ⁡ R ∈ NrmVec ↔ ringLMod ⁡ R ∈ NrmMod ∧ ringLMod ⁡ R ∈ LVec
4 3 biimpri ⊢ ringLMod ⁡ R ∈ NrmMod ∧ ringLMod ⁡ R ∈ LVec → ringLMod ⁡ R ∈ NrmVec
5 1 2 4 syl2an ⊢ R ∈ NrmRing ∧ R ∈ DivRing → ringLMod ⁡ R ∈ NrmVec