Metamath Proof Explorer

Theorem tngnrg

Description: Given any absolute value over a ring, augmenting the ring with the absolute value produces a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngnrg.t 
|- T = ( R toNrmGrp F )
tngnrg.a 
|- A = ( AbsVal ` R )
Assertion tngnrg 
|- ( F e. A -> T e. NrmRing )

Proof

Step Hyp Ref Expression
1 tngnrg.t 
 |-  T = ( R toNrmGrp F )
2 tngnrg.a 
 |-  A = ( AbsVal ` R )
3 2 abvrcl 
 |-  ( F e. A -> R e. Ring )
4 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
5 3 4 syl 
 |-  ( F e. A -> R e. Grp )
6 eqid 
 |-  ( -g ` R ) = ( -g ` R )
7 1 6 tngds 
 |-  ( F e. A -> ( F o. ( -g ` R ) ) = ( dist ` T ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 2 6 abvmet 
 |-  ( F e. A -> ( F o. ( -g ` R ) ) e. ( Met ` ( Base ` R ) ) )
10 7 9 eqeltrrd 
 |-  ( F e. A -> ( dist ` T ) e. ( Met ` ( Base ` R ) ) )
11 2 8 abvf 
 |-  ( F e. A -> F : ( Base ` R ) --> RR )
12 eqid 
 |-  ( dist ` T ) = ( dist ` T )
13 1 8 12 tngngp2 
 |-  ( F : ( Base ` R ) --> RR -> ( T e. NrmGrp <-> ( R e. Grp /\ ( dist ` T ) e. ( Met ` ( Base ` R ) ) ) ) )
14 11 13 syl 
 |-  ( F e. A -> ( T e. NrmGrp <-> ( R e. Grp /\ ( dist ` T ) e. ( Met ` ( Base ` R ) ) ) ) )
15 5 10 14 mpbir2and 
 |-  ( F e. A -> T e. NrmGrp )
16 reex 
 |-  RR e. _V
17 1 8 16 tngnm 
 |-  ( ( R e. Grp /\ F : ( Base ` R ) --> RR ) -> F = ( norm ` T ) )
18 5 11 17 syl2anc 
 |-  ( F e. A -> F = ( norm ` T ) )
19 eqidd 
 |-  ( F e. A -> ( Base ` R ) = ( Base ` R ) )
20 1 8 tngbas 
 |-  ( F e. A -> ( Base ` R ) = ( Base ` T ) )
21 eqid 
 |-  ( +g ` R ) = ( +g ` R )
22 1 21 tngplusg 
 |-  ( F e. A -> ( +g ` R ) = ( +g ` T ) )
23 22 oveqdr 
 |-  ( ( F e. A /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` T ) y ) )
24 eqid 
 |-  ( .r ` R ) = ( .r ` R )
25 1 24 tngmulr 
 |-  ( F e. A -> ( .r ` R ) = ( .r ` T ) )
26 25 oveqdr 
 |-  ( ( F e. A /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` T ) y ) )
27 19 20 23 26 abvpropd 
 |-  ( F e. A -> ( AbsVal ` R ) = ( AbsVal ` T ) )
28 2 27 syl5eq 
 |-  ( F e. A -> A = ( AbsVal ` T ) )
29 18 28 eleq12d 
 |-  ( F e. A -> ( F e. A <-> ( norm ` T ) e. ( AbsVal ` T ) ) )
30 29 ibi 
 |-  ( F e. A -> ( norm ` T ) e. ( AbsVal ` T ) )
31 eqid 
 |-  ( norm ` T ) = ( norm ` T )
32 eqid 
 |-  ( AbsVal ` T ) = ( AbsVal ` T )
33 31 32 isnrg 
 |-  ( T e. NrmRing <-> ( T e. NrmGrp /\ ( norm ` T ) e. ( AbsVal ` T ) ) )
34 15 30 33 sylanbrc 
 |-  ( F e. A -> T e. NrmRing )