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 e. NrmRing -> ( ringLMod ` R ) e. NrmMod )

Proof

Step Hyp Ref Expression
1 nrgring 
 |-  ( R e. NrmRing -> R e. Ring )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 2 subrgid 
 |-  ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
4 1 3 syl 
 |-  ( R e. NrmRing -> ( Base ` R ) e. ( SubRing ` R ) )
5 rlmval 
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
6 5 sranlm 
 |-  ( ( R e. NrmRing /\ ( Base ` R ) e. ( SubRing ` R ) ) -> ( ringLMod ` R ) e. NrmMod )
7 4 6 mpdan 
 |-  ( R e. NrmRing -> ( ringLMod ` R ) e. NrmMod )