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

Metamath Proof Explorer

Theorem nrmtngdist

Description: The augmentation of a normed group by its own norm has the same distance function as the normed group (restricted to the base set). (Contributed by AV, 15-Oct-2021)

Ref Expression
Hypotheses nrmtngdist.t 
|- T = ( G toNrmGrp ( norm ` G ) )
nrmtngdist.x 
|- X = ( Base ` G )
Assertion nrmtngdist 
|- ( G e. NrmGrp -> ( dist ` T ) = ( ( dist ` G ) |` ( X X. X ) ) )

Proof

Step Hyp Ref Expression
1 nrmtngdist.t 
 |-  T = ( G toNrmGrp ( norm ` G ) )
2 nrmtngdist.x 
 |-  X = ( Base ` G )
3 fvex 
 |-  ( norm ` G ) e. _V
4 eqid 
 |-  ( -g ` G ) = ( -g ` G )
5 1 4 tngds 
 |-  ( ( norm ` G ) e. _V -> ( ( norm ` G ) o. ( -g ` G ) ) = ( dist ` T ) )
6 3 5 ax-mp 
 |-  ( ( norm ` G ) o. ( -g ` G ) ) = ( dist ` T )
7 eqid 
 |-  ( norm ` G ) = ( norm ` G )
8 eqid 
 |-  ( dist ` G ) = ( dist ` G )
9 eqid 
 |-  ( ( dist ` G ) |` ( X X. X ) ) = ( ( dist ` G ) |` ( X X. X ) )
10 7 4 8 2 9 isngp2 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( ( norm ` G ) o. ( -g ` G ) ) = ( ( dist ` G ) |` ( X X. X ) ) ) )
11 10 simp3bi 
 |-  ( G e. NrmGrp -> ( ( norm ` G ) o. ( -g ` G ) ) = ( ( dist ` G ) |` ( X X. X ) ) )
12 6 11 eqtr3id 
 |-  ( G e. NrmGrp -> ( dist ` T ) = ( ( dist ` G ) |` ( X X. X ) ) )