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 xmet0
Description: The distance function of a metric space is zero if its arguments are
equal. Definition 14-1.1(a) of Gleason p. 223. (Contributed by Mario
Carneiro , 20-Aug-2015)
Ref
Expression
Assertion
xmet0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )
Proof
Step
Hyp
Ref
Expression
1
eqid ⊢ 𝐴 = 𝐴
2
xmeteq0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐴 ) = 0 ↔ 𝐴 = 𝐴 ) )
3
2
3anidm23 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐴 ) = 0 ↔ 𝐴 = 𝐴 ) )
4
1 3
mpbiri ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )