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 A T NrmRing

Proof

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