This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlmval2

Description: Value of the ring module extended. (Contributed by AV, 2-Dec-2018) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Assertion rlmval2 
|- ( W e. X -> ( ringLMod ` W ) = ( ( ( W sSet <. ( Scalar ` ndx ) , W >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )

Proof

Step Hyp Ref Expression
1 rlmval 
 |-  ( ringLMod ` W ) = ( ( subringAlg ` W ) ` ( Base ` W ) )
2 1 a1i 
 |-  ( W e. X -> ( ringLMod ` W ) = ( ( subringAlg ` W ) ` ( Base ` W ) ) )
3 ssid 
 |-  ( Base ` W ) C_ ( Base ` W )
4 sraval 
 |-  ( ( W e. X /\ ( Base ` W ) C_ ( Base ` W ) ) -> ( ( subringAlg ` W ) ` ( Base ` W ) ) = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s ( Base ` W ) ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
5 3 4 mpan2 
 |-  ( W e. X -> ( ( subringAlg ` W ) ` ( Base ` W ) ) = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s ( Base ` W ) ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 6 ressid 
 |-  ( W e. X -> ( W |`s ( Base ` W ) ) = W )
8 7 opeq2d 
 |-  ( W e. X -> <. ( Scalar ` ndx ) , ( W |`s ( Base ` W ) ) >. = <. ( Scalar ` ndx ) , W >. )
9 8 oveq2d 
 |-  ( W e. X -> ( W sSet <. ( Scalar ` ndx ) , ( W |`s ( Base ` W ) ) >. ) = ( W sSet <. ( Scalar ` ndx ) , W >. ) )
10 9 oveq1d 
 |-  ( W e. X -> ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s ( Base ` W ) ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) = ( ( W sSet <. ( Scalar ` ndx ) , W >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
11 10 oveq1d 
 |-  ( W e. X -> ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s ( Base ` W ) ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) = ( ( ( W sSet <. ( Scalar ` ndx ) , W >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
12 2 5 11 3eqtrd 
 |-  ( W e. X -> ( ringLMod ` W ) = ( ( ( W sSet <. ( Scalar ` ndx ) , W >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )