Theorem xmetgt0

Description: The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmetgt0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≠ 𝐵 ↔ 0 < ( 𝐴 𝐷 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xmetge0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )
2	1	biantrud	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) ≤ 0 ↔ ( ( 𝐴 𝐷 𝐵 ) ≤ 0 ∧ 0 ≤ ( 𝐴 𝐷 𝐵 ) ) ) )
3		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
4		0xr	⊢ 0 ∈ ℝ*
5		xrletri3	⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ ( ( 𝐴 𝐷 𝐵 ) ≤ 0 ∧ 0 ≤ ( 𝐴 𝐷 𝐵 ) ) ) )
6	3 4 5	sylancl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ ( ( 𝐴 𝐷 𝐵 ) ≤ 0 ∧ 0 ≤ ( 𝐴 𝐷 𝐵 ) ) ) )
7	2 6	bitr4d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) ≤ 0 ↔ ( 𝐴 𝐷 𝐵 ) = 0 ) )
8		xrlenlt	⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝐴 𝐷 𝐵 ) ≤ 0 ↔ ¬ 0 < ( 𝐴 𝐷 𝐵 ) ) )
9	3 4 8	sylancl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) ≤ 0 ↔ ¬ 0 < ( 𝐴 𝐷 𝐵 ) ) )
10		xmeteq0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) )
11	7 9 10	3bitr3d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ¬ 0 < ( 𝐴 𝐷 𝐵 ) ↔ 𝐴 = 𝐵 ) )
12	11	necon1abid	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≠ 𝐵 ↔ 0 < ( 𝐴 𝐷 𝐵 ) ) )