Theorem mgpds

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

	Ref	Expression
Hypotheses	mgpbas.1	$$⊢M={\mathrm{mulGrp}}_R$$
	mgpds.2	$$⊢B=\mathrm{dist}\left(R\right)$$
Assertion	mgpds	$$⊢B=\mathrm{dist}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	$$⊢M={\mathrm{mulGrp}}_R$$
2		mgpds.2	$$⊢B=\mathrm{dist}\left(R\right)$$
3		eqid	$$⊢{\cdot }_R={\cdot }_R$$
4	1 3	mgpval	$$⊢M=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_R⟩$$
5		dsid	$$⊢\mathrm{dist}=\mathrm{Slot}\mathrm{dist}\left(\mathrm{ndx}\right)$$
6		dsndxnplusgndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
7	4 5 6	setsplusg	$$⊢\mathrm{dist}\left(R\right)=\mathrm{dist}\left(M\right)$$
8	2 7	eqtri	$$⊢B=\mathrm{dist}\left(M\right)$$