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

Metamath Proof Explorer

Theorem ngpmet

Description: The (induced) metric of a normed group is a metric. Part of Definition 2.2-1 of Kreyszig p. 58. (Contributed by NM, 4-Dec-2006) (Revised by AV, 14-Oct-2021)

	Ref	Expression
Hypotheses	ngpmet.x	$⊢ X = {Base}_{G}$
	ngpmet.d	$⊢ D = {dist (G) ↾}_{(X \times X)}$
Assertion	ngpmet	$⊢ G \in NrmGrp \to D \in Met (X)$

Proof

Step	Hyp	Ref	Expression
1		ngpmet.x	$⊢ X = {Base}_{G}$
2		ngpmet.d	$⊢ D = {dist (G) ↾}_{(X \times X)}$
3		ngpms	$⊢ G \in NrmGrp \to G \in MetSp$
4	1 2	msmet	$⊢ G \in MetSp \to D \in Met (X)$
5	3 4	syl	$⊢ G \in NrmGrp \to D \in Met (X)$