This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Basic metric space properties metgt0
Description: The distance function of a metric space is positive for unequal points.
Definition 14-1.1(b) of Gleason p. 223 and its converse. (Contributed by NM , 27-Aug-2006)
Ref
Expression
Assertion
metgt0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≠ 𝐵 ↔ 0 < ( 𝐴 𝐷 𝐵 ) ) )
Proof
Step
Hyp
Ref
Expression
1
metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2
xmetgt0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≠ 𝐵 ↔ 0 < ( 𝐴 𝐷 𝐵 ) ) )
3
1 2
syl3an1 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≠ 𝐵 ↔ 0 < ( 𝐴 𝐷 𝐵 ) ) )