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 ) ) ) |
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 ) ) ) |