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
 |-  ( T. -> ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) )
3 ssidd
 |-  ( T. -> ( Base ` R ) C_ ( Base ` R ) )
4 2 3 sratopn
 |-  ( T. -> ( TopOpen ` R ) = ( TopOpen ` ( ringLMod ` R ) ) )
5 4 mptru
 |-  ( TopOpen ` R ) = ( TopOpen ` ( ringLMod ` R ) )