ngpds2

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	ngpds2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = (A \underset{˙}{-} B) 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		eqid	$⊢ norm (G) = norm (G)$
6	5 1 3 4	ngpds	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = norm (G) (A \underset{˙}{-} B)$
7		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
8	1 3	grpsubcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
9	7 8	syl3an1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
10	5 1 2 4	nmval	$⊢ A \underset{˙}{-} B \in X \to norm (G) (A \underset{˙}{-} B) = (A \underset{˙}{-} B) D \underset{˙}{0}$
11	9 10	syl	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to norm (G) (A \underset{˙}{-} B) = (A \underset{˙}{-} B) D \underset{˙}{0}$
12	6 11	eqtrd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = (A \underset{˙}{-} B) D \underset{˙}{0}$

Metamath Proof Explorer