ngpds3

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	ngpds3	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = \underset{˙}{0} D (A \underset{˙}{-} B)$

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	1 2 3 4	ngpds2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = (A \underset{˙}{-} B) D \underset{˙}{0}$
6		ngpxms	$⊢ G \in NrmGrp \to G \in ∞MetSp$
7	6	3ad2ant1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to G \in ∞MetSp$
8		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
9	1 3	grpsubcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
10	8 9	syl3an1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
11	8	3ad2ant1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to G \in Grp$
12	1 2	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in X$
13	11 12	syl	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to \underset{˙}{0} \in X$
14	1 4	xmssym	$⊢ (G \in ∞MetSp \land A \underset{˙}{-} B \in X \land \underset{˙}{0} \in X) \to (A \underset{˙}{-} B) D \underset{˙}{0} = \underset{˙}{0} D (A \underset{˙}{-} B)$
15	7 10 13 14	syl3anc	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to (A \underset{˙}{-} B) D \underset{˙}{0} = \underset{˙}{0} D (A \underset{˙}{-} B)$
16	5 15	eqtrd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = \underset{˙}{0} D (A \underset{˙}{-} B)$

Metamath Proof Explorer