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

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