This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )