This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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