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 e. NrmRing /\ R e. DivRing ) -> ( ringLMod ` R ) e. NrmVec )

Proof

Step Hyp Ref Expression
1 rlmnlm 
 |-  ( R e. NrmRing -> ( ringLMod ` R ) e. NrmMod )
2 rlmlvec 
 |-  ( R e. DivRing -> ( ringLMod ` R ) e. LVec )
3 isnvc 
 |-  ( ( ringLMod ` R ) e. NrmVec <-> ( ( ringLMod ` R ) e. NrmMod /\ ( ringLMod ` R ) e. LVec ) )
4 3 biimpri 
 |-  ( ( ( ringLMod ` R ) e. NrmMod /\ ( ringLMod ` R ) e. LVec ) -> ( ringLMod ` R ) e. NrmVec )
5 1 2 4 syl2an 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> ( ringLMod ` R ) e. NrmVec )