Theorem distspace

Description: A set X together with a (distance) function D which is a pseudometric is adistance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set X equipped with adistance D , which is a mapping of two elements of the base set to the (extended) reals and which is nonnegative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021) (Revised by AV, 5-Jul-2022)

	Ref	Expression
Assertion	distspace	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ( 𝐴 𝐷 𝐴 ) = 0 ) ∧ ( 0 ≤ ( 𝐴 𝐷 𝐵 ) ∧ ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psmetf	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
2	1	3ad2ant1	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
3		psmet0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )
4	3	3adant3	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )
5	2 4	jca	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ( 𝐴 𝐷 𝐴 ) = 0 ) )
6		psmetge0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )
7		psmetsym	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
8	5 6 7	jca32	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ( 𝐴 𝐷 𝐴 ) = 0 ) ∧ ( 0 ≤ ( 𝐴 𝐷 𝐵 ) ∧ ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) ) ) )