Metamath Proof Explorer

Theorem rlmlmod

Description: The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014)

Ref Expression
Assertion rlmlmod 
|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )

Proof

Step Hyp Ref Expression
1 rlmval 
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 2 subrgid 
 |-  ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
4 eqid 
 |-  ( ( subringAlg ` R ) ` ( Base ` R ) ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
5 4 sralmod 
 |-  ( ( Base ` R ) e. ( SubRing ` R ) -> ( ( subringAlg ` R ) ` ( Base ` R ) ) e. LMod )
6 3 5 syl 
 |-  ( R e. Ring -> ( ( subringAlg ` R ) ` ( Base ` R ) ) e. LMod )
7 1 6 eqeltrid 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )