Theorem xmeteq0

Description: The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmeteq0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) )

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		simpl	⊢ ( ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
6	5	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
7	4 6	simpl2im	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
8		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑦 ) )
9	8	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( 𝐴 𝐷 𝑦 ) = 0 ) )
10		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝑦 ) )
11	9 10	bibi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ↔ ( ( 𝐴 𝐷 𝑦 ) = 0 ↔ 𝐴 = 𝑦 ) ) )
12		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 𝐷 𝐵 ) )
13	12	eqeq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐷 𝑦 ) = 0 ↔ ( 𝐴 𝐷 𝐵 ) = 0 ) )
14		eqeq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐵 ) )
15	13 14	bibi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 𝐷 𝑦 ) = 0 ↔ 𝐴 = 𝑦 ) ↔ ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) ) )
16	11 15	rspc2v	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) ) )
17	7 16	syl5com	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) ) )
18	17	3impib	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) )