Metamath Proof Explorer

Theorem psmettri2

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

Ref Expression
Assertion psmettri2 ⊢D∈PsMet⁡X∧C∈X∧A∈X∧B∈X→ADB≤CDA+𝑒CDB

Proof

Step Hyp Ref Expression
1 elfvex ⊢D∈PsMet⁡X→X∈V
2 ispsmet ⊢X∈V→D∈PsMet⁡X↔D:X×X⟶ℝ*∧∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
3 1 2 syl ⊢D∈PsMet⁡X→D∈PsMet⁡X↔D:X×X⟶ℝ*∧∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
4 3 ibi ⊢D∈PsMet⁡X→D:X×X⟶ℝ*∧∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
5 4 simprd ⊢D∈PsMet⁡X→∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
6 5 r19.21bi ⊢D∈PsMet⁡X∧a∈X→aDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
7 6 simprd ⊢D∈PsMet⁡X∧a∈X→∀b∈X∀c∈XaDb≤cDa+𝑒cDb
8 7 ralrimiva ⊢D∈PsMet⁡X→∀a∈X∀b∈X∀c∈XaDb≤cDa+𝑒cDb
9 oveq1 ⊢a=A→aDb=ADb
10 oveq2 ⊢a=A→cDa=cDA
11 10 oveq1d ⊢a=A→cDa+𝑒cDb=cDA+𝑒cDb
12 9 11 breq12d ⊢a=A→aDb≤cDa+𝑒cDb↔ADb≤cDA+𝑒cDb
13 oveq2 ⊢b=B→ADb=ADB
14 oveq2 ⊢b=B→cDb=cDB
15 14 oveq2d ⊢b=B→cDA+𝑒cDb=cDA+𝑒cDB
16 13 15 breq12d ⊢b=B→ADb≤cDA+𝑒cDb↔ADB≤cDA+𝑒cDB
17 oveq1 ⊢c=C→cDA=CDA
18 oveq1 ⊢c=C→cDB=CDB
19 17 18 oveq12d ⊢c=C→cDA+𝑒cDB=CDA+𝑒CDB
20 19 breq2d ⊢c=C→ADB≤cDA+𝑒cDB↔ADB≤CDA+𝑒CDB
21 12 16 20 rspc3v ⊢A∈X∧B∈X∧C∈X→∀a∈X∀b∈X∀c∈XaDb≤cDa+𝑒cDb→ADB≤CDA+𝑒CDB
22 21 3comr ⊢C∈X∧A∈X∧B∈X→∀a∈X∀b∈X∀c∈XaDb≤cDa+𝑒cDb→ADB≤CDA+𝑒CDB
23 8 22 mpan9 ⊢D∈PsMet⁡X∧C∈X∧A∈X∧B∈X→ADB≤CDA+𝑒CDB