Theorem ngpds

Description: Value of the distance function in terms of the norm of a normed group. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (Revised 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	ngpds	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to ADB=N\left(A\underset{\dot{}}{-}B\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		eqid	$$⊢{D\upharpoonright }_{\left(X\times X\right)}={D\upharpoonright }_{\left(X\times X\right)}$$
6	1 3 4 2 5	isngp2	$$⊢G\in \mathrm{NrmGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{MetSp}\wedge N\circ \underset{\dot{}}{-}={D\upharpoonright }_{\left(X\times X\right)}\right)$$
7	6	simp3bi	$$⊢G\in \mathrm{NrmGrp}\to N\circ \underset{\dot{}}{-}={D\upharpoonright }_{\left(X\times X\right)}$$
8	7	3ad2ant1	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to N\circ \underset{\dot{}}{-}={D\upharpoonright }_{\left(X\times X\right)}$$
9	8	oveqd	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to A\left(N\circ \underset{\dot{}}{-}\right)B=A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B$$
10		ngpgrp	$$⊢G\in \mathrm{NrmGrp}\to G\in \mathrm{Grp}$$
11	2 3	grpsubf	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{-}:X\times X⟶X$$
12	10 11	syl	$$⊢G\in \mathrm{NrmGrp}\to \underset{\dot{}}{-}:X\times X⟶X$$
13	12	3ad2ant1	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to \underset{\dot{}}{-}:X\times X⟶X$$
14		opelxpi	$$⊢\left(A\in X\wedge B\in X\right)\to ⟨A,B⟩\in \left(X\times X\right)$$
15	14	3adant1	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to ⟨A,B⟩\in \left(X\times X\right)$$
16		fvco3	$$⊢\left(\underset{\dot{}}{-}:X\times X⟶X\wedge ⟨A,B⟩\in \left(X\times X\right)\right)\to \left(N\circ \underset{\dot{}}{-}\right)\left(⟨A,B⟩\right)=N\left(\underset{\dot{}}{-}\left(⟨A,B⟩\right)\right)$$
17	13 15 16	syl2anc	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to \left(N\circ \underset{\dot{}}{-}\right)\left(⟨A,B⟩\right)=N\left(\underset{\dot{}}{-}\left(⟨A,B⟩\right)\right)$$
18		df-ov	$$⊢A\left(N\circ \underset{\dot{}}{-}\right)B=\left(N\circ \underset{\dot{}}{-}\right)\left(⟨A,B⟩\right)$$
19		df-ov	$$⊢A\underset{\dot{}}{-}B=\underset{\dot{}}{-}\left(⟨A,B⟩\right)$$
20	19	fveq2i	$$⊢N\left(A\underset{\dot{}}{-}B\right)=N\left(\underset{\dot{}}{-}\left(⟨A,B⟩\right)\right)$$
21	17 18 20	3eqtr4g	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to A\left(N\circ \underset{\dot{}}{-}\right)B=N\left(A\underset{\dot{}}{-}B\right)$$
22		ovres	$$⊢\left(A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$
23	22	3adant1	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$
24	9 21 23	3eqtr3rd	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge B\in X\right)\to ADB=N\left(A\underset{\dot{}}{-}B\right)$$