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 syl6bi ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ 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 → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )