Database
BASIC TOPOLOGY
Metric spaces
Examples of metric spaces
abvmet
Metamath Proof Explorer
Description: An absolute value F generates a metric defined by
d ( x , y ) = F ( x - y ) , analogously to cnmet . (In fact, the
ring structure is not needed at all; the group properties abveq0 and
abvtri , abvneg are sufficient.) (Contributed by Mario Carneiro , 9-Sep-2014) (Revised by Mario Carneiro , 2-Oct-2015)
Ref
Expression
Hypotheses
abvmet.x
⊢ X = Base R
abvmet.a
⊢ A = AbsVal ⁡ R
abvmet.m
⊢ - ˙ = - R
Assertion
abvmet
⊢ F ∈ A → F ∘ - ˙ ∈ Met ⁡ X
Proof
Step
Hyp
Ref
Expression
1
abvmet.x
⊢ X = Base R
2
abvmet.a
⊢ A = AbsVal ⁡ R
3
abvmet.m
⊢ - ˙ = - R
4
eqid
⊢ 0 R = 0 R
5
2
abvrcl
⊢ F ∈ A → R ∈ Ring
6
ringgrp
⊢ R ∈ Ring → R ∈ Grp
7
5 6
syl
⊢ F ∈ A → R ∈ Grp
8
2 1
abvf
⊢ F ∈ A → F : X ⟶ ℝ
9
2 1 4
abveq0
⊢ F ∈ A ∧ x ∈ X → F ⁡ x = 0 ↔ x = 0 R
10
2 1 3
abvsubtri
⊢ F ∈ A ∧ x ∈ X ∧ y ∈ X → F ⁡ x - ˙ y ≤ F ⁡ x + F ⁡ y
11
10
3expb
⊢ F ∈ A ∧ x ∈ X ∧ y ∈ X → F ⁡ x - ˙ y ≤ F ⁡ x + F ⁡ y
12
1 3 4 7 8 9 11
nrmmetd
⊢ F ∈ A → F ∘ - ˙ ∈ Met ⁡ X