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={\mathrm{Base}}_G$$
	ngpmet.d	$$⊢D={\mathrm{dist}\left(G\right)\upharpoonright }_{\left(X\times X\right)}$$
Assertion	ngpmet	$$⊢G\in \mathrm{NrmGrp}\to D\in \mathrm{Met}\left(X\right)$$

Proof

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