Metamath Proof Explorer

Theorem rlmscaf

Description: Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Assertion rlmscaf 
|- ( +f ` ( mulGrp ` R ) ) = ( .sf ` ( ringLMod ` R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 1 2 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 1 4 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
6 eqid 
 |-  ( +f ` ( mulGrp ` R ) ) = ( +f ` ( mulGrp ` R ) )
7 3 5 6 plusffval 
 |-  ( +f ` ( mulGrp ` R ) ) = ( x e. ( Base ` R ) , y e. ( Base ` R ) |-> ( x ( .r ` R ) y ) )
8 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
9 rlmsca2 
 |-  ( _I ` R ) = ( Scalar ` ( ringLMod ` R ) )
10 df-base 
 |-  Base = Slot 1
11 10 2 strfvi 
 |-  ( Base ` R ) = ( Base ` ( _I ` R ) )
12 eqid 
 |-  ( .sf ` ( ringLMod ` R ) ) = ( .sf ` ( ringLMod ` R ) )
13 rlmvsca 
 |-  ( .r ` R ) = ( .s ` ( ringLMod ` R ) )
14 8 9 11 12 13 scaffval 
 |-  ( .sf ` ( ringLMod ` R ) ) = ( x e. ( Base ` R ) , y e. ( Base ` R ) |-> ( x ( .r ` R ) y ) )
15 7 14 eqtr4i 
 |-  ( +f ` ( mulGrp ` R ) ) = ( .sf ` ( ringLMod ` R ) )