Metamath Proof Explorer

Theorem nrmtngdist

Description: The augmentation of a normed group by its own norm has the same distance function as the normed group (restricted to the base set). (Contributed by AV, 15-Oct-2021)

Ref Expression
Hypotheses nrmtngdist.t ⊢ T = G toNrmGrp norm ⁡ G
nrmtngdist.x ⊢ X = Base G
Assertion nrmtngdist ⊢ G ∈ NrmGrp → dist ⁡ T = dist ⁡ G ↾ X × X

Proof

Step Hyp Ref Expression
1 nrmtngdist.t ⊢ T = G toNrmGrp norm ⁡ G
2 nrmtngdist.x ⊢ X = Base G
3 fvex ⊢ norm ⁡ G ∈ V
4 eqid ⊢ - G = - G
5 1 4 tngds ⊢ norm ⁡ G ∈ V → norm ⁡ G ∘ - G = dist ⁡ T
6 3 5 ax-mp ⊢ norm ⁡ G ∘ - G = dist ⁡ T
7 eqid ⊢ norm ⁡ G = norm ⁡ G
8 eqid ⊢ dist ⁡ G = dist ⁡ G
9 eqid ⊢ dist ⁡ G ↾ X × X = dist ⁡ G ↾ X × X
10 7 4 8 2 9 isngp2 ⊢ G ∈ NrmGrp ↔ G ∈ Grp ∧ G ∈ MetSp ∧ norm ⁡ G ∘ - G = dist ⁡ G ↾ X × X
11 10 simp3bi ⊢ G ∈ NrmGrp → norm ⁡ G ∘ - G = dist ⁡ G ↾ X × X
12 6 11 eqtr3id ⊢ G ∈ NrmGrp → dist ⁡ T = dist ⁡ G ↾ X × X