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 ‘ 𝑅 ) )