Metamath Proof Explorer


Theorem rlmplusg

Description: Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Assertion rlmplusg ( +g𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rlmval ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
2 1 a1i ( ⊤ → ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) )
3 ssidd ( ⊤ → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
4 2 3 sraaddg ( ⊤ → ( +g𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) ) )
5 4 mptru ( +g𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )