Database
BASIC ALGEBRAIC STRUCTURES
Ideals
The subring algebra; ideals
rlmtopn
Next ⟩
rlmds
Metamath Proof Explorer
Ascii
Unicode
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