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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	ngpmet.d	⊢ 𝐷 = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion	ngpmet	⊢ ( 𝐺 ∈ NrmGrp → 𝐷 ∈ ( Met ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ngpmet.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		ngpmet.d	⊢ 𝐷 = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
3		ngpms	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
4	1 2	msmet	⊢ ( 𝐺 ∈ MetSp → 𝐷 ∈ ( Met ‘ 𝑋 ) )
5	3 4	syl	⊢ ( 𝐺 ∈ NrmGrp → 𝐷 ∈ ( Met ‘ 𝑋 ) )