Metamath Proof Explorer

Theorem tngngpd

Description: Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngngp.t 
|- T = ( G toNrmGrp N )
tngngp.x 
|- X = ( Base ` G )
tngngp.m 
|- .- = ( -g ` G )
tngngp.z 
|- .0. = ( 0g ` G )
tngngpd.1 
|- ( ph -> G e. Grp )
tngngpd.2 
|- ( ph -> N : X --> RR )
tngngpd.3 
|- ( ( ph /\ x e. X ) -> ( ( N ` x ) = 0 <-> x = .0. ) )
tngngpd.4 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
Assertion tngngpd 
|- ( ph -> T e. NrmGrp )

Proof

Step Hyp Ref Expression
1 tngngp.t 
 |-  T = ( G toNrmGrp N )
2 tngngp.x 
 |-  X = ( Base ` G )
3 tngngp.m 
 |-  .- = ( -g ` G )
4 tngngp.z 
 |-  .0. = ( 0g ` G )
5 tngngpd.1 
 |-  ( ph -> G e. Grp )
6 tngngpd.2 
 |-  ( ph -> N : X --> RR )
7 tngngpd.3 
 |-  ( ( ph /\ x e. X ) -> ( ( N ` x ) = 0 <-> x = .0. ) )
8 tngngpd.4 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
9 2 fvexi 
 |-  X e. _V
10 reex 
 |-  RR e. _V
11 fex2 
 |-  ( ( N : X --> RR /\ X e. _V /\ RR e. _V ) -> N e. _V )
12 9 10 11 mp3an23 
 |-  ( N : X --> RR -> N e. _V )
13 1 3 tngds 
 |-  ( N e. _V -> ( N o. .- ) = ( dist ` T ) )
14 6 12 13 3syl 
 |-  ( ph -> ( N o. .- ) = ( dist ` T ) )
15 2 3 4 5 6 7 8 nrmmetd 
 |-  ( ph -> ( N o. .- ) e. ( Met ` X ) )
16 14 15 eqeltrrd 
 |-  ( ph -> ( dist ` T ) e. ( Met ` X ) )
17 eqid 
 |-  ( dist ` T ) = ( dist ` T )
18 1 2 17 tngngp2 
 |-  ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ ( dist ` T ) e. ( Met ` X ) ) ) )
19 6 18 syl 
 |-  ( ph -> ( T e. NrmGrp <-> ( G e. Grp /\ ( dist ` T ) e. ( Met ` X ) ) ) )
20 5 16 19 mpbir2and 
 |-  ( ph -> T e. NrmGrp )