Description: Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | rlmtopn | |- ( TopOpen ` R ) = ( TopOpen ` ( ringLMod ` R ) ) |
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 ) ) |