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		df-ds	$$⊢\mathrm{dist}=\mathrm{Slot}12$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5		2nn	$$⊢2\in \mathbb{N}$$
6	4 5	decnncl	$$⊢12\in \mathbb{N}$$
7		2re	$$⊢2\in ℝ$$
8		1nn	$$⊢1\in \mathbb{N}$$
9		2nn0	$$⊢2\in {\mathbb{N}}_0$$
10		2lt10	$$⊢2<10$$
11	8 9 9 10	declti	$$⊢2<12$$
12	7 11	gtneii	$$⊢12\ne 2$$
13	1 3 6 12	mgplem	$$⊢\mathrm{dist}\left(R\right)=\mathrm{dist}\left(M\right)$$
14	2 13	eqtri	$$⊢B=\mathrm{dist}\left(M\right)$$