This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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