Metamath Proof Explorer


Theorem mettri2

Description: Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion mettri2 DMetXCXAXBXADBCDA+CDB

Proof

Step Hyp Ref Expression
1 metxmet DMetXD∞MetX
2 xmettri2 D∞MetXCXAXBXADBCDA+𝑒CDB
3 1 2 sylan DMetXCXAXBXADBCDA+𝑒CDB
4 metcl DMetXCXAXCDA
5 4 3adant3r3 DMetXCXAXBXCDA
6 metcl DMetXCXBXCDB
7 6 3adant3r2 DMetXCXAXBXCDB
8 5 7 rexaddd DMetXCXAXBXCDA+𝑒CDB=CDA+CDB
9 3 8 breqtrd DMetXCXAXBXADBCDA+CDB