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 eqtrid ⊢ 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