Metamath Proof Explorer

Theorem rlmnlm

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

Ref Expression
Assertion rlmnlm ⊢ R ∈ NrmRing → ringLMod ⁡ R ∈ NrmMod

Proof

Step Hyp Ref Expression
1 nrgring ⊢ R ∈ NrmRing → R ∈ Ring
2 eqid ⊢ Base R = Base R
3 2 subrgid ⊢ R ∈ Ring → Base R ∈ SubRing ⁡ R
4 1 3 syl ⊢ R ∈ NrmRing → Base R ∈ SubRing ⁡ R
5 rlmval ⊢ ringLMod ⁡ R = subringAlg ⁡ R ⁡ Base R
6 5 sranlm ⊢ R ∈ NrmRing ∧ Base R ∈ SubRing ⁡ R → ringLMod ⁡ R ∈ NrmMod
7 4 6 mpdan ⊢ R ∈ NrmRing → ringLMod ⁡ R ∈ NrmMod