This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Examples of metric spaces abvmet
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 ⊢ 𝑋 = ( Base ‘ 𝑅 )
abvmet.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
abvmet.m ⊢ − = ( -g ‘ 𝑅 )
Assertion
abvmet ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) )
Proof
Step
Hyp
Ref
Expression
1
abvmet.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
2
abvmet.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
3
abvmet.m ⊢ − = ( -g ‘ 𝑅 )
4
eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5
2
abvrcl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )
6
ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
7
5 6
syl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Grp )
8
2 1
abvf ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : 𝑋 ⟶ ℝ )
9
2 1 4
abveq0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑅 ) ) )
10
2 1 3
abvsubtri ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
11
10
3expb ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
12
1 3 4 7 8 9 11
nrmmetd ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) )