Metamath Proof Explorer


Theorem rlmscaf

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

Ref Expression
Assertion rlmscaf ( +๐‘“ โ€˜ ( mulGrp โ€˜ ๐‘… ) ) = ( ยทsf โ€˜ ( ringLMod โ€˜ ๐‘… ) )

Proof

Step Hyp Ref Expression
1 eqid โŠข ( mulGrp โ€˜ ๐‘… ) = ( mulGrp โ€˜ ๐‘… )
2 eqid โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ๐‘… )
3 1 2 mgpbas โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ( mulGrp โ€˜ ๐‘… ) )
4 eqid โŠข ( .r โ€˜ ๐‘… ) = ( .r โ€˜ ๐‘… )
5 1 4 mgpplusg โŠข ( .r โ€˜ ๐‘… ) = ( +g โ€˜ ( mulGrp โ€˜ ๐‘… ) )
6 eqid โŠข ( +๐‘“ โ€˜ ( mulGrp โ€˜ ๐‘… ) ) = ( +๐‘“ โ€˜ ( mulGrp โ€˜ ๐‘… ) )
7 3 5 6 plusffval โŠข ( +๐‘“ โ€˜ ( mulGrp โ€˜ ๐‘… ) ) = ( ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘… ) , ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘… ) โ†ฆ ( ๐‘ฅ ( .r โ€˜ ๐‘… ) ๐‘ฆ ) )
8 rlmbas โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ( ringLMod โ€˜ ๐‘… ) )
9 rlmsca2 โŠข ( I โ€˜ ๐‘… ) = ( Scalar โ€˜ ( ringLMod โ€˜ ๐‘… ) )
10 baseid โŠข Base = Slot ( Base โ€˜ ndx )
11 10 2 strfvi โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ( I โ€˜ ๐‘… ) )
12 eqid โŠข ( ยทsf โ€˜ ( ringLMod โ€˜ ๐‘… ) ) = ( ยทsf โ€˜ ( ringLMod โ€˜ ๐‘… ) )
13 rlmvsca โŠข ( .r โ€˜ ๐‘… ) = ( ยท๐‘  โ€˜ ( ringLMod โ€˜ ๐‘… ) )
14 8 9 11 12 13 scaffval โŠข ( ยทsf โ€˜ ( ringLMod โ€˜ ๐‘… ) ) = ( ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘… ) , ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘… ) โ†ฆ ( ๐‘ฅ ( .r โ€˜ ๐‘… ) ๐‘ฆ ) )
15 7 14 eqtr4i โŠข ( +๐‘“ โ€˜ ( mulGrp โ€˜ ๐‘… ) ) = ( ยทsf โ€˜ ( ringLMod โ€˜ ๐‘… ) )