Metamath Proof Explorer


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