Metamath Proof Explorer


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 DPsMetXAXBXD:X×X*ADA=00ADBADB=BDA

Proof

Step Hyp Ref Expression
1 psmetf DPsMetXD:X×X*
2 1 3ad2ant1 DPsMetXAXBXD:X×X*
3 psmet0 DPsMetXAXADA=0
4 3 3adant3 DPsMetXAXBXADA=0
5 2 4 jca DPsMetXAXBXD:X×X*ADA=0
6 psmetge0 DPsMetXAXBX0ADB
7 psmetsym DPsMetXAXBXADB=BDA
8 5 6 7 jca32 DPsMetXAXBXD:X×X*ADA=00ADBADB=BDA