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 \in NrmGrp \to dist (T) = {dist (G) ↾}_{(X \times X)}$

Proof

Step	Hyp	Ref	Expression
1		nrmtngdist.t	$⊢ T = G toNrmGrp norm (G)$
2		nrmtngdist.x	$⊢ X = {Base}_{G}$
3		fvex	$⊢ norm (G) \in V$
4		eqid	$⊢ -_{G} = -_{G}$
5	1 4	tngds	$⊢ norm (G) \in V \to norm (G) \circ -_{G} = dist (T)$
6	3 5	ax-mp	$⊢ norm (G) \circ -_{G} = dist (T)$
7		eqid	$⊢ norm (G) = norm (G)$
8		eqid	$⊢ dist (G) = dist (G)$
9		eqid	$⊢ {dist (G) ↾}_{(X \times X)} = {dist (G) ↾}_{(X \times X)}$
10	7 4 8 2 9	isngp2	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land norm (G) \circ -_{G} = {dist (G) ↾}_{(X \times X)})$
11	10	simp3bi	$⊢ G \in NrmGrp \to norm (G) \circ -_{G} = {dist (G) ↾}_{(X \times X)}$
12	6 11	eqtr3id	$⊢ G \in NrmGrp \to dist (T) = {dist (G) ↾}_{(X \times X)}$