Metamath Proof Explorer

Theorem mgptset

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

Ref Expression
Hypothesis mgpbas.1 
|- M = ( mulGrp ` R )
Assertion mgptset 
|- ( TopSet ` R ) = ( TopSet ` M )

Proof

Step Hyp Ref Expression
1 mgpbas.1 
 |-  M = ( mulGrp ` R )
2 eqid 
 |-  ( .r ` R ) = ( .r ` R )
3 1 2 mgpval 
 |-  M = ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. )
4 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
5 tsetndxnplusgndx 
 |-  ( TopSet ` ndx ) =/= ( +g ` ndx )
6 3 4 5 setsplusg 
 |-  ( TopSet ` R ) = ( TopSet ` M )