Metamath Proof Explorer

Theorem psmettri2

Description: Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +e ( 𝐶 𝐷 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
2 ispsmet ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) ) ) ) )
3 1 2 syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) ) ) ) )
4 3 ibi ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) ) ) )
5 4 simprd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) ) )
6 5 r19.21bi ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) ) )
7 6 simprd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) → ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) )
8 7 ralrimiva ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) )
9 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 𝐷 𝑏 ) = ( 𝐴 𝐷 𝑏 ) )
10 oveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑐 𝐷 𝑎 ) = ( 𝑐 𝐷 𝐴 ) )
11 10 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) = ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝑏 ) ) )
12 9 11 breq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) ↔ ( 𝐴 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝑏 ) ) ) )
13 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 𝐷 𝑏 ) = ( 𝐴 𝐷 𝐵 ) )
14 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝑐 𝐷 𝑏 ) = ( 𝑐 𝐷 𝐵 ) )
15 14 oveq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝑏 ) ) = ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝐵 ) ) )
16 13 15 breq12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝑏 ) ) ↔ ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝐵 ) ) ) )
17 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 𝐷 𝐴 ) = ( 𝐶 𝐷 𝐴 ) )
18 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 𝐷 𝐵 ) = ( 𝐶 𝐷 𝐵 ) )
19 17 18 oveq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝐵 ) ) = ( ( 𝐶 𝐷 𝐴 ) +e ( 𝐶 𝐷 𝐵 ) ) )
20 19 breq2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝑐 𝐷 𝐴 ) +e ( 𝑐 𝐷 𝐵 ) ) ↔ ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +e ( 𝐶 𝐷 𝐵 ) ) ) )
21 12 16 20 rspc3v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +e ( 𝐶 𝐷 𝐵 ) ) ) )
22 21 3comr ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +e ( 𝑐 𝐷 𝑏 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +e ( 𝐶 𝐷 𝐵 ) ) ) )
23 8 22 mpan9 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +e ( 𝐶 𝐷 𝐵 ) ) )