Metamath Proof Explorer


Theorem psmetge0

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

Ref Expression
Assertion psmetge0 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2 simp2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → 𝐴𝑋 )
3 simp3 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → 𝐵𝑋 )
4 psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐵𝑋 ) ) → ( 𝐵 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
5 1 2 3 3 4 syl13anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐵 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
6 2re 2 ∈ ℝ
7 rexr ( 2 ∈ ℝ → 2 ∈ ℝ* )
8 xmul01 ( 2 ∈ ℝ* → ( 2 ·e 0 ) = 0 )
9 6 7 8 mp2b ( 2 ·e 0 ) = 0
10 psmet0 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 0 )
11 10 3adant2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 0 )
12 9 11 eqtr4id ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 2 ·e 0 ) = ( 𝐵 𝐷 𝐵 ) )
13 psmetcl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
14 x2times ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* → ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
15 13 14 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
16 5 12 15 3brtr4d ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 2 ·e 0 ) ≤ ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) )
17 0xr 0 ∈ ℝ*
18 2rp 2 ∈ ℝ+
19 18 a1i ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → 2 ∈ ℝ+ )
20 xlemul2 ( ( 0 ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ 2 ∈ ℝ+ ) → ( 0 ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 2 ·e 0 ) ≤ ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) ) )
21 17 13 19 20 mp3an2i ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 0 ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 2 ·e 0 ) ≤ ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) ) )
22 16 21 mpbird ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )