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 metsym
Description: The distance function of a metric space is symmetric. Definition
14-1.1(c) of Gleason p. 223. (Contributed by NM , 27-Aug-2006)
(Revised by Mario Carneiro , 20-Aug-2015)
Ref
Expression
Assertion
metsym ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2
xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
3
1 2
syl3an1 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )