Metamath Proof Explorer


Theorem rlmbas

Description: Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Assertion rlmbas ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )

Proof

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