Metamath Proof Explorer

Theorem rlmsca2

Description: Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Assertion rlmsca2 
|- ( _I ` R ) = ( Scalar ` ( ringLMod ` R ) )

Proof

Step Hyp Ref Expression
1 fvi 
 |-  ( R e. _V -> ( _I ` R ) = R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 2 ressid 
 |-  ( R e. _V -> ( R |`s ( Base ` R ) ) = R )
4 1 3 eqtr4d 
 |-  ( R e. _V -> ( _I ` R ) = ( R |`s ( Base ` R ) ) )
5 fvprc 
 |-  ( -. R e. _V -> ( _I ` R ) = (/) )
6 reldmress 
 |-  Rel dom |`s
7 6 ovprc1 
 |-  ( -. R e. _V -> ( R |`s ( Base ` R ) ) = (/) )
8 5 7 eqtr4d 
 |-  ( -. R e. _V -> ( _I ` R ) = ( R |`s ( Base ` R ) ) )
9 4 8 pm2.61i 
 |-  ( _I ` R ) = ( R |`s ( Base ` R ) )
10 rlmval 
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
11 10 a1i 
 |-  ( T. -> ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) )
12 ssidd 
 |-  ( T. -> ( Base ` R ) C_ ( Base ` R ) )
13 11 12 srasca 
 |-  ( T. -> ( R |`s ( Base ` R ) ) = ( Scalar ` ( ringLMod ` R ) ) )
14 13 mptru 
 |-  ( R |`s ( Base ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
15 9 14 eqtri 
 |-  ( _I ` R ) = ( Scalar ` ( ringLMod ` R ) )