Database
BASIC TOPOLOGY
Metric spaces
Normed algebraic structures
ngpmet
Metamath Proof Explorer
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 × X
Assertion
ngpmet
⊢ G ∈ NrmGrp → D ∈ Met ⁡ X
Proof
Step
Hyp
Ref
Expression
1
ngpmet.x
⊢ X = Base G
2
ngpmet.d
⊢ D = dist ⁡ G ↾ X × X
3
ngpms
⊢ G ∈ NrmGrp → G ∈ MetSp
4
1 2
msmet
⊢ G ∈ MetSp → D ∈ Met ⁡ X
5
3 4
syl
⊢ G ∈ NrmGrp → D ∈ Met ⁡ X