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

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)$

Step	Hyp	Ref	Expression
1		mgpbas.1	$⊢ M = {mulGrp}_{R}$
2		eqid	$⊢ \cdot_{R} = \cdot_{R}$
3	1 2	mgpval	$⊢ M = R sSet ⟨+_{ndx}, \cdot_{R}⟩$
4		tsetid	$⊢ TopSet = Slot TopSet (ndx)$
5		tsetndxnplusgndx	$⊢ TopSet (ndx) \neq +_{ndx}$
6	3 4 5	setsplusg	$⊢ TopSet (R) = TopSet (M)$