This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑋 ) )