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 ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) ) )