This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Normed algebraic structures 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 ‘ 𝑋 ) )