Theorem mgptset

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

	Ref	Expression
Hypothesis	mgpbas.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	mgptset	⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
3	1 2	mgpval	⊢ 𝑀 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ )
4		tsetid	⊢ TopSet = Slot ( TopSet ‘ ndx )
5		tsetndxnplusgndx	⊢ ( TopSet ‘ ndx ) ≠ ( +g ‘ ndx )
6	3 4 5	setsplusg	⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑀 )