Theorem ngpds3r

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={\mathrm{Base}}_G$$
	ngpds2.z	$$⊢\underset{\dot{}}{0}=0_G$$
	ngpds2.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	ngpds2.d	$$⊢D=\mathrm{dist}\left(G\right)$$
Assertion	ngpds3r	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to ADB=\underset{\dot{}}{0}D\left(B\underset{\dot{}}{-}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ngpds2.x	$$⊢X={\mathrm{Base}}_G$$
2		ngpds2.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		ngpds2.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		ngpds2.d	$$⊢D=\mathrm{dist}\left(G\right)$$
5		ngpxms	$$⊢G\in \mathrm{NrmGrp}\to G\in \mathrm{\infty MetSp}$$
6	1 4	xmssym	$$⊢\left(G\in \mathrm{\infty MetSp}\wedge A\in X\wedge B\in X\right)\to ADB=BDA$$
7	5 6	syl3an1	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to ADB=BDA$$
8	1 2 3 4	ngpds3	$$⊢\left(G\in \mathrm{NrmGrp}\wedge B\in X\wedge A\in X\right)\to BDA=\underset{\dot{}}{0}D\left(B\underset{\dot{}}{-}A\right)$$
9	8	3com23	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to BDA=\underset{\dot{}}{0}D\left(B\underset{\dot{}}{-}A\right)$$
10	7 9	eqtrd	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to ADB=\underset{\dot{}}{0}D\left(B\underset{\dot{}}{-}A\right)$$