Metamath Proof Explorer


Theorem psmettri

Description: Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion psmettri DPsMetXAXBXCXADBADC+𝑒CDB

Proof

Step Hyp Ref Expression
1 simpl DPsMetXAXBXCXDPsMetX
2 simpr3 DPsMetXAXBXCXCX
3 simpr1 DPsMetXAXBXCXAX
4 simpr2 DPsMetXAXBXCXBX
5 psmettri2 DPsMetXCXAXBXADBCDA+𝑒CDB
6 1 2 3 4 5 syl13anc DPsMetXAXBXCXADBCDA+𝑒CDB
7 psmetsym DPsMetXCXAXCDA=ADC
8 1 2 3 7 syl3anc DPsMetXAXBXCXCDA=ADC
9 8 oveq1d DPsMetXAXBXCXCDA+𝑒CDB=ADC+𝑒CDB
10 6 9 breqtrd DPsMetXAXBXCXADBADC+𝑒CDB