ngpdsr

Description: Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	ngpds.n	$⊢ N = norm (G)$
	ngpds.x	$⊢ X = {Base}_{G}$
	ngpds.m	$⊢ \underset{˙}{-} = -_{G}$
	ngpds.d	$⊢ D = dist (G)$
Assertion	ngpdsr	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = N (B \underset{˙}{-} A)$

Step	Hyp	Ref	Expression
1		ngpds.n	$⊢ N = norm (G)$
2		ngpds.x	$⊢ X = {Base}_{G}$
3		ngpds.m	$⊢ \underset{˙}{-} = -_{G}$
4		ngpds.d	$⊢ D = dist (G)$
5		ngpxms	$⊢ G \in NrmGrp \to G \in ∞MetSp$
6	2 4	xmssym	$⊢ (G \in ∞MetSp \land A \in X \land B \in X) \to A D B = B D A$
7	5 6	syl3an1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = B D A$
8	1 2 3 4	ngpds	$⊢ (G \in NrmGrp \land B \in X \land A \in X) \to B D A = N (B \underset{˙}{-} A)$
9	8	3com23	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to B D A = N (B \underset{˙}{-} A)$
10	7 9	eqtrd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = N (B \underset{˙}{-} A)$

Metamath Proof Explorer