Metamath Proof Explorer


Theorem mgptopn

Description: Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses mgpbas.1 𝑀 = ( mulGrp ‘ 𝑅 )
mgptopn.2 𝐽 = ( TopOpen ‘ 𝑅 )
Assertion mgptopn 𝐽 = ( TopOpen ‘ 𝑀 )

Proof

Step Hyp Ref Expression
1 mgpbas.1 𝑀 = ( mulGrp ‘ 𝑅 )
2 mgptopn.2 𝐽 = ( TopOpen ‘ 𝑅 )
3 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑅 )
5 3 4 topnval ( ( TopSet ‘ 𝑅 ) ↾t ( Base ‘ 𝑅 ) ) = ( TopOpen ‘ 𝑅 )
6 1 3 mgpbas ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
7 1 mgptset ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑀 )
8 6 7 topnval ( ( TopSet ‘ 𝑅 ) ↾t ( Base ‘ 𝑅 ) ) = ( TopOpen ‘ 𝑀 )
9 2 5 8 3eqtr2i 𝐽 = ( TopOpen ‘ 𝑀 )