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 = ( norm ` G )
	ngpds.x	|- X = ( Base ` G )
	ngpds.m	|- .- = ( -g ` G )
	ngpds.d	|- D = ( dist ` G )
Assertion	ngpds	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A .- B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ngpds.n	|- N = ( norm ` G )
2		ngpds.x	|- X = ( Base ` G )
3		ngpds.m	|- .- = ( -g ` G )
4		ngpds.d	|- D = ( dist ` G )
5		eqid	|- ( D |` ( X X. X ) ) = ( D |` ( X X. X ) )
6	1 3 4 2 5	isngp2	|- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = ( D |` ( X X. X ) ) ) )
7	6	simp3bi	|- ( G e. NrmGrp -> ( N o. .- ) = ( D |` ( X X. X ) ) )
8	7	3ad2ant1	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N o. .- ) = ( D |` ( X X. X ) ) )
9	8	oveqd	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A ( N o. .- ) B ) = ( A ( D |` ( X X. X ) ) B ) )
10		ngpgrp	|- ( G e. NrmGrp -> G e. Grp )
11	2 3	grpsubf	|- ( G e. Grp -> .- : ( X X. X ) --> X )
12	10 11	syl	|- ( G e. NrmGrp -> .- : ( X X. X ) --> X )
13	12	3ad2ant1	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> .- : ( X X. X ) --> X )
14		opelxpi	|- ( ( A e. X /\ B e. X ) -> <. A , B >. e. ( X X. X ) )
15	14	3adant1	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> <. A , B >. e. ( X X. X ) )
16		fvco3	|- ( ( .- : ( X X. X ) --> X /\ <. A , B >. e. ( X X. X ) ) -> ( ( N o. .- ) ` <. A , B >. ) = ( N ` ( .- ` <. A , B >. ) ) )
17	13 15 16	syl2anc	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N o. .- ) ` <. A , B >. ) = ( N ` ( .- ` <. A , B >. ) ) )
18		df-ov	|- ( A ( N o. .- ) B ) = ( ( N o. .- ) ` <. A , B >. )
19		df-ov	|- ( A .- B ) = ( .- ` <. A , B >. )
20	19	fveq2i	|- ( N ` ( A .- B ) ) = ( N ` ( .- ` <. A , B >. ) )
21	17 18 20	3eqtr4g	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A ( N o. .- ) B ) = ( N ` ( A .- B ) ) )
22		ovres	|- ( ( A e. X /\ B e. X ) -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) )
23	22	3adant1	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) )
24	9 21 23	3eqtr3rd	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A .- B ) ) )