Metamath Proof Explorer


Theorem rlmtopn

Description: Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Assertion rlmtopn TopOpen R = TopOpen ringLMod R

Proof

Step Hyp Ref Expression
1 rlmval ringLMod R = subringAlg R Base R
2 1 a1i ringLMod R = subringAlg R Base R
3 ssidd Base R Base R
4 2 3 sratopn TopOpen R = TopOpen ringLMod R
5 4 mptru TopOpen R = TopOpen ringLMod R