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		df-ds	|- dist = Slot ; 1 2
4		1nn0	|- 1 e. NN0
5		2nn	|- 2 e. NN
6	4 5	decnncl	|- ; 1 2 e. NN
7		2re	|- 2 e. RR
8		1nn	|- 1 e. NN
9		2nn0	|- 2 e. NN0
10		2lt10	|- 2 < ; 1 0
11	8 9 9 10	declti	|- 2 < ; 1 2
12	7 11	gtneii	|- ; 1 2 =/= 2
13	1 3 6 12	mgplem	|- ( dist ` R ) = ( dist ` M )
14	2 13	eqtri	|- B = ( dist ` M )