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

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 ⊢ 𝑇 = ( 𝐺 toNrmGrp ( norm ‘ 𝐺 ) )
nrmtngdist.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion nrmtngdist ( 𝐺 ∈ NrmGrp → ( dist ‘ 𝑇 ) = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) ) )

Proof

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