Theorem mgpds

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

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

Proof

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