rlmscaf

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

		Ref	Expression
	Assertion	rlmscaf	$⊢ +_{𝑓} ({mulGrp}_{R}) = \cdot_{𝑠𝑓} (ringLMod (R))$

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	$⊢ \cdot_{R} = \cdot_{R}$
5	1 4	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
6		eqid	$⊢ +_{𝑓} ({mulGrp}_{R}) = +_{𝑓} ({mulGrp}_{R})$
7	3 5 6	plusffval	$⊢ +_{𝑓} ({mulGrp}_{R}) = (x \in {Base}_{R}, y \in {Base}_{R} ⟼ x \cdot_{R} y)$
8		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
9		rlmsca2	$⊢ I (R) = Scalar (ringLMod (R))$
10		baseid	$⊢ Base = Slot {Base}_{ndx}$
11	10 2	strfvi	$⊢ {Base}_{R} = {Base}_{I (R)}$
12		eqid	$⊢ \cdot_{𝑠𝑓} (ringLMod (R)) = \cdot_{𝑠𝑓} (ringLMod (R))$
13		rlmvsca	$⊢ \cdot_{R} = \cdot_{ringLMod (R)}$
14	8 9 11 12 13	scaffval	$⊢ \cdot_{𝑠𝑓} (ringLMod (R)) = (x \in {Base}_{R}, y \in {Base}_{R} ⟼ x \cdot_{R} y)$
15	7 14	eqtr4i	$⊢ +_{𝑓} ({mulGrp}_{R}) = \cdot_{𝑠𝑓} (ringLMod (R))$

Metamath Proof Explorer