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 ⊢ T = G toNrmGrp N
tngngpim.n ⊢ N = norm ⁡ G
tngngpim.x ⊢ X = Base G
tngngpim.d ⊢ D = dist ⁡ T
Assertion tngngpim ⊢ G ∈ NrmGrp → D : X × X ⟶ ℝ

Proof

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