Metamath Proof Explorer


Theorem rlmbas

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

Ref Expression
Assertion rlmbas BaseR=BaseringLModR

Proof

Step Hyp Ref Expression
1 rlmval ringLModR=subringAlgRBaseR
2 1 a1i ringLModR=subringAlgRBaseR
3 ssidd BaseRBaseR
4 2 3 srabase BaseR=BaseringLModR
5 4 mptru BaseR=BaseringLModR