Theorem mgpds

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

	Ref	Expression
Hypotheses	mgpbas.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	mgpds.2	⊢ 𝐵 = ( dist ‘ 𝑅 )
Assertion	mgpds	⊢ 𝐵 = ( dist ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		mgpds.2	⊢ 𝐵 = ( dist ‘ 𝑅 )
3		df-ds	⊢ dist = Slot ; 1 2
4		1nn0	⊢ 1 ∈ ℕ0
5		2nn	⊢ 2 ∈ ℕ
6	4 5	decnncl	⊢ ; 1 2 ∈ ℕ
7		2re	⊢ 2 ∈ ℝ
8		1nn	⊢ 1 ∈ ℕ
9		2nn0	⊢ 2 ∈ ℕ0
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 ‘ 𝑅 ) = ( dist ‘ 𝑀 )
14	2 13	eqtri	⊢ 𝐵 = ( dist ‘ 𝑀 )