Metamath Proof Explorer

Theorem nrmtngnrm

Description: The augmentation of a normed group by its own norm is a normed group with the same norm. (Contributed by AV, 15-Oct-2021)

Ref Expression
Hypothesis nrmtngdist.t 
|- T = ( G toNrmGrp ( norm ` G ) )
Assertion nrmtngnrm 
|- ( G e. NrmGrp -> ( T e. NrmGrp /\ ( norm ` T ) = ( norm ` G ) ) )

Proof

Step Hyp Ref Expression
1 nrmtngdist.t 
 |-  T = ( G toNrmGrp ( norm ` G ) )
2 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 1 3 nrmtngdist 
 |-  ( G e. NrmGrp -> ( dist ` T ) = ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) )
5 eqid 
 |-  ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) = ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) )
6 3 5 ngpmet 
 |-  ( G e. NrmGrp -> ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( Met ` ( Base ` G ) ) )
7 4 6 eqeltrd 
 |-  ( G e. NrmGrp -> ( dist ` T ) e. ( Met ` ( Base ` G ) ) )
8 eqid 
 |-  ( norm ` G ) = ( norm ` G )
9 3 8 nmf 
 |-  ( G e. NrmGrp -> ( norm ` G ) : ( Base ` G ) --> RR )
10 eqid 
 |-  ( dist ` T ) = ( dist ` T )
11 1 3 10 tngngp2 
 |-  ( ( norm ` G ) : ( Base ` G ) --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ ( dist ` T ) e. ( Met ` ( Base ` G ) ) ) ) )
12 9 11 syl 
 |-  ( G e. NrmGrp -> ( T e. NrmGrp <-> ( G e. Grp /\ ( dist ` T ) e. ( Met ` ( Base ` G ) ) ) ) )
13 2 7 12 mpbir2and 
 |-  ( G e. NrmGrp -> T e. NrmGrp )
14 2 9 jca 
 |-  ( G e. NrmGrp -> ( G e. Grp /\ ( norm ` G ) : ( Base ` G ) --> RR ) )
15 reex 
 |-  RR e. _V
16 1 3 15 tngnm 
 |-  ( ( G e. Grp /\ ( norm ` G ) : ( Base ` G ) --> RR ) -> ( norm ` G ) = ( norm ` T ) )
17 14 16 syl 
 |-  ( G e. NrmGrp -> ( norm ` G ) = ( norm ` T ) )
18 17 eqcomd 
 |-  ( G e. NrmGrp -> ( norm ` T ) = ( norm ` G ) )
19 13 18 jca 
 |-  ( G e. NrmGrp -> ( T e. NrmGrp /\ ( norm ` T ) = ( norm ` G ) ) )