Theorem ngpdsr

Description: Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	ngpds.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	ngpds.x	$$⊢X={\mathrm{Base}}_G$$
	ngpds.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	ngpds.d	$$⊢D=\mathrm{dist}\left(G\right)$$
Assertion	ngpdsr	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to ADB=N\left(B\underset{\dot{}}{-}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ngpds.n	$$⊢N=\mathrm{norm}\left(G\right)$$
2		ngpds.x	$$⊢X={\mathrm{Base}}_G$$
3		ngpds.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		ngpds.d	$$⊢D=\mathrm{dist}\left(G\right)$$
5		ngpxms	$$⊢G\in \mathrm{NrmGrp}\to G\in \mathrm{\infty MetSp}$$
6	2 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	ngpds	$$⊢\left(G\in \mathrm{NrmGrp}\wedge B\in X\wedge A\in X\right)\to BDA=N\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=N\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=N\left(B\underset{\dot{}}{-}A\right)$$