Metamath Proof Explorer

Theorem psmetsym

Description: The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetsym ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )

Proof

Step Hyp Ref Expression
1 psmetcl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
2 psmetcl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) ∈ ℝ* )
3 2 3com23 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) ∈ ℝ* )
4 simp1 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
5 simp3 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
6 simp2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
7 psmettri2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐵 ) ) )
8 4 5 6 5 7 syl13anc ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐵 ) ) )
9 psmet0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 0 )
10 9 3adant2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 0 )
11 10 oveq2d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐵 ) ) = ( ( 𝐵 𝐷 𝐴 ) +𝑒 0 ) )
12 2 xaddid1d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 0 ) = ( 𝐵 𝐷 𝐴 ) )
13 12 3com23 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 0 ) = ( 𝐵 𝐷 𝐴 ) )
14 11 13 eqtrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐵 ) ) = ( 𝐵 𝐷 𝐴 ) )
15 8 14 breqtrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ≤ ( 𝐵 𝐷 𝐴 ) )
16 psmettri2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐴 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐴 ) ) )
17 4 6 5 6 16 syl13anc ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐴 ) ) )
18 psmet0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )
19 18 3adant3 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )
20 19 oveq2d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐴 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) )
21 1 xaddid1d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐴 𝐷 𝐵 ) )
22 20 21 eqtrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐴 ) ) = ( 𝐴 𝐷 𝐵 ) )
23 17 22 breqtrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) ≤ ( 𝐴 𝐷 𝐵 ) )
24 1 3 15 23 xrletrid ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )