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 e. NrmGrp -> ( dist ` T ) = ( ( dist ` G ) |` ( X 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 ) e. _V
4		eqid	|- ( -g ` G ) = ( -g ` G )
5	1 4	tngds	|- ( ( norm ` G ) e. _V -> ( ( norm ` G ) o. ( -g ` G ) ) = ( dist ` T ) )
6	3 5	ax-mp	|- ( ( norm ` G ) o. ( -g ` G ) ) = ( dist ` T )
7		eqid	|- ( norm ` G ) = ( norm ` G )
8		eqid	|- ( dist ` G ) = ( dist ` G )
9		eqid	|- ( ( dist ` G ) |` ( X X. X ) ) = ( ( dist ` G ) |` ( X X. X ) )
10	7 4 8 2 9	isngp2	|- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( ( norm ` G ) o. ( -g ` G ) ) = ( ( dist ` G ) |` ( X X. X ) ) ) )
11	10	simp3bi	|- ( G e. NrmGrp -> ( ( norm ` G ) o. ( -g ` G ) ) = ( ( dist ` G ) |` ( X X. X ) ) )
12	6 11	eqtr3id	|- ( G e. NrmGrp -> ( dist ` T ) = ( ( dist ` G ) |` ( X X. X ) ) )