This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tngngpd

Description: Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngngp.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngngp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
tngngp.m ⊢ − = ( -g ‘ 𝐺 )
tngngp.z ⊢ 0 = ( 0g ‘ 𝐺 )
tngngpd.1 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
tngngpd.2 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ ℝ )
tngngpd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
tngngpd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
Assertion tngngpd ( 𝜑 → 𝑇 ∈ NrmGrp )

Proof

Step Hyp Ref Expression
1 tngngp.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngngp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 tngngp.m ⊢ − = ( -g ‘ 𝐺 )
4 tngngp.z ⊢ 0 = ( 0g ‘ 𝐺 )
5 tngngpd.1 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
6 tngngpd.2 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ ℝ )
7 tngngpd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
8 tngngpd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
9 2 fvexi ⊢ 𝑋 ∈ V
10 reex ⊢ ℝ ∈ V
11 fex2 ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑋 ∈ V ∧ ℝ ∈ V ) → 𝑁 ∈ V )
12 9 10 11 mp3an23 ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → 𝑁 ∈ V )
13 1 3 tngds ⊢ ( 𝑁 ∈ V → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
14 6 12 13 3syl ⊢ ( 𝜑 → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
15 2 3 4 5 6 7 8 nrmmetd ⊢ ( 𝜑 → ( 𝑁 ∘ − ) ∈ ( Met ‘ 𝑋 ) )
16 14 15 eqeltrrd ⊢ ( 𝜑 → ( dist ‘ 𝑇 ) ∈ ( Met ‘ 𝑋 ) )
17 eqid ⊢ ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
18 1 2 17 tngngp2 ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ 𝑋 ) ) ) )
19 6 18 syl ⊢ ( 𝜑 → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ 𝑋 ) ) ) )
20 5 16 19 mpbir2and ⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )