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