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 ⊢ 𝑇 = ( 𝑅 toNrmGrp 𝐹 )
tngnrg.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
Assertion tngnrg ( 𝐹 ∈ 𝐴 → 𝑇 ∈ NrmRing )

Proof

Step Hyp Ref Expression
1 tngnrg.t ⊢ 𝑇 = ( 𝑅 toNrmGrp 𝐹 )
2 tngnrg.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
3 2 abvrcl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )
4 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
5 3 4 syl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Grp )
6 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
7 1 6 tngds ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∘ ( -g ‘ 𝑅 ) ) = ( dist ‘ 𝑇 ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 2 6 abvmet ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∘ ( -g ‘ 𝑅 ) ) ∈ ( Met ‘ ( Base ‘ 𝑅 ) ) )
10 7 9 eqeltrrd ⊢ ( 𝐹 ∈ 𝐴 → ( dist ‘ 𝑇 ) ∈ ( Met ‘ ( Base ‘ 𝑅 ) ) )
11 2 8 abvf ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ℝ )
12 eqid ⊢ ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
13 1 8 12 tngngp2 ⊢ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝑅 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ ( Base ‘ 𝑅 ) ) ) ) )
14 11 13 syl ⊢ ( 𝐹 ∈ 𝐴 → ( 𝑇 ∈ NrmGrp ↔ ( 𝑅 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ ( Base ‘ 𝑅 ) ) ) ) )
15 5 10 14 mpbir2and ⊢ ( 𝐹 ∈ 𝐴 → 𝑇 ∈ NrmGrp )
16 reex ⊢ ℝ ∈ V
17 1 8 16 tngnm ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 : ( Base ‘ 𝑅 ) ⟶ ℝ ) → 𝐹 = ( norm ‘ 𝑇 ) )
18 5 11 17 syl2anc ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 = ( norm ‘ 𝑇 ) )
19 eqidd ⊢ ( 𝐹 ∈ 𝐴 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
20 1 8 tngbas ⊢ ( 𝐹 ∈ 𝐴 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑇 ) )
21 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
22 1 21 tngplusg ⊢ ( 𝐹 ∈ 𝐴 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑇 ) )
23 22 oveqdr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
24 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
25 1 24 tngmulr ⊢ ( 𝐹 ∈ 𝐴 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑇 ) )
26 25 oveqdr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) )
27 19 20 23 26 abvpropd ⊢ ( 𝐹 ∈ 𝐴 → ( AbsVal ‘ 𝑅 ) = ( AbsVal ‘ 𝑇 ) )
28 2 27 eqtrid ⊢ ( 𝐹 ∈ 𝐴 → 𝐴 = ( AbsVal ‘ 𝑇 ) )
29 18 28 eleq12d ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∈ 𝐴 ↔ ( norm ‘ 𝑇 ) ∈ ( AbsVal ‘ 𝑇 ) ) )
30 29 ibi ⊢ ( 𝐹 ∈ 𝐴 → ( norm ‘ 𝑇 ) ∈ ( AbsVal ‘ 𝑇 ) )
31 eqid ⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
32 eqid ⊢ ( AbsVal ‘ 𝑇 ) = ( AbsVal ‘ 𝑇 )
33 31 32 isnrg ⊢ ( 𝑇 ∈ NrmRing ↔ ( 𝑇 ∈ NrmGrp ∧ ( norm ‘ 𝑇 ) ∈ ( AbsVal ‘ 𝑇 ) ) )
34 15 30 33 sylanbrc ⊢ ( 𝐹 ∈ 𝐴 → 𝑇 ∈ NrmRing )