Metamath Proof Explorer

Theorem xmettri2

Description: Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmettri2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
2 isxmet ⊢ ( 𝑋 ∈ dom ∞Met → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
3 1 2 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
4 3 ibi ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
5 simpr ⊢ ( ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
6 5 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
7 4 6 simpl2im ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
8 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑦 ) )
9 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑧 𝐷 𝑥 ) = ( 𝑧 𝐷 𝐴 ) )
10 9 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
11 8 10 breq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ( 𝐴 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
12 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 𝐷 𝐵 ) )
13 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑧 𝐷 𝑦 ) = ( 𝑧 𝐷 𝐵 ) )
14 13 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝐵 ) ) )
15 12 14 breq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝐵 ) ) ) )
16 oveq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 𝐷 𝐴 ) = ( 𝐶 𝐷 𝐴 ) )
17 oveq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 𝐷 𝐵 ) = ( 𝐶 𝐷 𝐵 ) )
18 16 17 oveq12d ⊢ ( 𝑧 = 𝐶 → ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝐵 ) ) = ( ( 𝐶 𝐷 𝐴 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) )
19 18 breq2d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝑧 𝐷 𝐴 ) +𝑒 ( 𝑧 𝐷 𝐵 ) ) ↔ ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) ) )
20 11 15 19 rspc3v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) ) )
21 7 20 syl5 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) ) )
22 21 3comr ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) ) )
23 22 impcom ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) )