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

Metamath Proof Explorer

Theorem tngngpim

Description: The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021)

Ref Expression
Hypotheses tngngpim.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngngpim.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
tngngpim.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
tngngpim.d ⊢ 𝐷 = ( dist ‘ 𝑇 )
Assertion tngngpim ( 𝐺 ∈ NrmGrp → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 tngngpim.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngngpim.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 tngngpim.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
4 tngngpim.d ⊢ 𝐷 = ( dist ‘ 𝑇 )
5 3 2 nmf ⊢ ( 𝐺 ∈ NrmGrp → 𝑁 : 𝑋 ⟶ ℝ )
6 2 oveq2i ⊢ ( 𝐺 toNrmGrp 𝑁 ) = ( 𝐺 toNrmGrp ( norm ‘ 𝐺 ) )
7 1 6 eqtri ⊢ 𝑇 = ( 𝐺 toNrmGrp ( norm ‘ 𝐺 ) )
8 7 nrmtngnrm ⊢ ( 𝐺 ∈ NrmGrp → ( 𝑇 ∈ NrmGrp ∧ ( norm ‘ 𝑇 ) = ( norm ‘ 𝐺 ) ) )
9 1 3 4 tngngp2 ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) )
10 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
11 9 10 biimtrdi ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
12 11 com12 ⊢ ( 𝑇 ∈ NrmGrp → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
13 12 adantr ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( norm ‘ 𝑇 ) = ( norm ‘ 𝐺 ) ) → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
14 8 13 syl ⊢ ( 𝐺 ∈ NrmGrp → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
15 metf ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
16 14 15 syl6 ⊢ ( 𝐺 ∈ NrmGrp → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
17 5 16 mpd ⊢ ( 𝐺 ∈ NrmGrp → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )