Theorem mgpbas

Description: Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014) (Revised by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	mgpbas.1	|- M = ( mulGrp ` R )
	mgpbas.2	|- B = ( Base ` R )
Assertion	mgpbas	|- B = ( Base ` M )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	|- M = ( mulGrp ` R )
2		mgpbas.2	|- B = ( Base ` R )
3		eqid	|- ( .r ` R ) = ( .r ` R )
4	1 3	mgpval	|- M = ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. )
5		baseid	|- Base = Slot ( Base ` ndx )
6		basendxnplusgndx	|- ( Base ` ndx ) =/= ( +g ` ndx )
7	4 5 6	setsplusg	|- ( Base ` R ) = ( Base ` M )
8	2 7	eqtri	|- B = ( Base ` M )