Metamath Proof Explorer


Theorem isxmetd

Description: Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by AV, 9-Apr-2024)

Ref Expression
Hypotheses isxmetd.0 ( 𝜑𝑋𝑉 )
isxmetd.1 ( 𝜑𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
isxmetd.2 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
isxmetd.3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
Assertion isxmetd ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 isxmetd.0 ( 𝜑𝑋𝑉 )
2 isxmetd.1 ( 𝜑𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
3 isxmetd.2 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
4 isxmetd.3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
5 4 3exp2 ( 𝜑 → ( 𝑥𝑋 → ( 𝑦𝑋 → ( 𝑧𝑋 → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
6 5 imp32 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑧𝑋 → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
7 6 ralrimiv ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
8 3 7 jca ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
9 8 ralrimivva ( 𝜑 → ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
10 isxmet ( 𝑋𝑉 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
11 1 10 syl ( 𝜑 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
12 2 9 11 mpbir2and ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )