Theorem rlmscaf

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

	Ref	Expression
Assertion	rlmscaf	$$⊢{+}_{𝑓}\left({\mathrm{mulGrp}}_R\right)={\cdot }_{\mathrm{𝑠𝑓}}\left(\mathrm{ringLMod}\left(R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3	1 2	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
4		eqid	$$⊢{\cdot }_R={\cdot }_R$$
5	1 4	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
6		eqid	$$⊢{+}_{𝑓}\left({\mathrm{mulGrp}}_R\right)={+}_{𝑓}\left({\mathrm{mulGrp}}_R\right)$$
7	3 5 6	plusffval	$$⊢{+}_{𝑓}\left({\mathrm{mulGrp}}_R\right)=\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_R⟼x{\cdot }_{R}y\right)$$
8		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
9		rlmsca2	$$⊢\mathrm{I}\left(R\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
10		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
11	10 2	strfvi	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{I}\left(R\right)}$$
12		eqid	$$⊢{\cdot }_{\mathrm{𝑠𝑓}}\left(\mathrm{ringLMod}\left(R\right)\right)={\cdot }_{\mathrm{𝑠𝑓}}\left(\mathrm{ringLMod}\left(R\right)\right)$$
13		rlmvsca	$$⊢{\cdot }_R={\cdot }_{\mathrm{ringLMod}\left(R\right)}$$
14	8 9 11 12 13	scaffval	$$⊢{\cdot }_{\mathrm{𝑠𝑓}}\left(\mathrm{ringLMod}\left(R\right)\right)=\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_R⟼x{\cdot }_{R}y\right)$$
15	7 14	eqtr4i	$$⊢{+}_{𝑓}\left({\mathrm{mulGrp}}_R\right)={\cdot }_{\mathrm{𝑠𝑓}}\left(\mathrm{ringLMod}\left(R\right)\right)$$