ngpds2r

Description: Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	ngpds2.x	$⊢ X = {Base}_{G}$
	ngpds2.z	$⊢ \underset{˙}{0} = 0_{G}$
	ngpds2.m	$⊢ \underset{˙}{-} = -_{G}$
	ngpds2.d	$⊢ D = dist (G)$
Assertion	ngpds2r	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = (B \underset{˙}{-} A) D \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		ngpds2.x	$⊢ X = {Base}_{G}$
2		ngpds2.z	$⊢ \underset{˙}{0} = 0_{G}$
3		ngpds2.m	$⊢ \underset{˙}{-} = -_{G}$
4		ngpds2.d	$⊢ D = dist (G)$
5		ngpxms	$⊢ G \in NrmGrp \to G \in ∞MetSp$
6	1 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	ngpds2	$⊢ (G \in NrmGrp \land B \in X \land A \in X) \to B D A = (B \underset{˙}{-} A) D \underset{˙}{0}$
9	8	3com23	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to B D A = (B \underset{˙}{-} A) D \underset{˙}{0}$
10	7 9	eqtrd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = (B \underset{˙}{-} A) D \underset{˙}{0}$

Metamath Proof Explorer