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 RNrmRingringLModRNrmMod

Proof

Step Hyp Ref Expression
1 nrgring RNrmRingRRing
2 eqid BaseR=BaseR
3 2 subrgid RRingBaseRSubRingR
4 1 3 syl RNrmRingBaseRSubRingR
5 rlmval ringLModR=subringAlgRBaseR
6 5 sranlm RNrmRingBaseRSubRingRringLModRNrmMod
7 4 6 mpdan RNrmRingringLModRNrmMod