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