Metamath Proof Explorer


Theorem rlmsca

Description: Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014)

Ref Expression
Assertion rlmsca
|- ( R e. X -> R = ( Scalar ` ( ringLMod ` R ) ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( Base ` R ) = ( Base ` R )
2 1 ressid
 |-  ( R e. X -> ( R |`s ( Base ` R ) ) = R )
3 rlmval
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
4 3 a1i
 |-  ( R e. X -> ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) )
5 ssidd
 |-  ( R e. X -> ( Base ` R ) C_ ( Base ` R ) )
6 4 5 srasca
 |-  ( R e. X -> ( R |`s ( Base ` R ) ) = ( Scalar ` ( ringLMod ` R ) ) )
7 2 6 eqtr3d
 |-  ( R e. X -> R = ( Scalar ` ( ringLMod ` R ) ) )