Database
BASIC ALGEBRAIC STRUCTURES
Rings
Multiplicative Group
mgptopn
Next ⟩
mgpds
Metamath Proof Explorer
Ascii
Unicode
Theorem
mgptopn
Description:
Topology of the multiplication group.
(Contributed by
Mario Carneiro
, 5-Oct-2015)
Ref
Expression
Hypotheses
mgpbas.1
⊢
M
=
mulGrp
R
mgptopn.2
⊢
J
=
TopOpen
⁡
R
Assertion
mgptopn
⊢
J
=
TopOpen
⁡
M
Proof
Step
Hyp
Ref
Expression
1
mgpbas.1
⊢
M
=
mulGrp
R
2
mgptopn.2
⊢
J
=
TopOpen
⁡
R
3
eqid
⊢
Base
R
=
Base
R
4
eqid
⊢
TopSet
⁡
R
=
TopSet
⁡
R
5
3
4
topnval
⊢
TopSet
⁡
R
↾
𝑡
Base
R
=
TopOpen
⁡
R
6
1
3
mgpbas
⊢
Base
R
=
Base
M
7
1
mgptset
⊢
TopSet
⁡
R
=
TopSet
⁡
M
8
6
7
topnval
⊢
TopSet
⁡
R
↾
𝑡
Base
R
=
TopOpen
⁡
M
9
2
5
8
3eqtr2i
⊢
J
=
TopOpen
⁡
M