Metamath Proof Explorer

Theorem xmettri2

Description: Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmettri2 ⊢D∈∞Met⁡X∧C∈X∧A∈X∧B∈X→ADB≤CDA+𝑒CDB

Proof

Step Hyp Ref Expression
1 elfvdm ⊢D∈∞Met⁡X→X∈dom⁡∞Met
2 isxmet ⊢X∈dom⁡∞Met→D∈∞Met⁡X↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
3 1 2 syl ⊢D∈∞Met⁡X→D∈∞Met⁡X↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
4 3 ibi ⊢D∈∞Met⁡X→D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
5 simpr ⊢xDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy→∀z∈XxDy≤zDx+𝑒zDy
6 5 2ralimi ⊢∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy→∀x∈X∀y∈X∀z∈XxDy≤zDx+𝑒zDy
7 4 6 simpl2im ⊢D∈∞Met⁡X→∀x∈X∀y∈X∀z∈XxDy≤zDx+𝑒zDy
8 oveq1 ⊢x=A→xDy=ADy
9 oveq2 ⊢x=A→zDx=zDA
10 9 oveq1d ⊢x=A→zDx+𝑒zDy=zDA+𝑒zDy
11 8 10 breq12d ⊢x=A→xDy≤zDx+𝑒zDy↔ADy≤zDA+𝑒zDy
12 oveq2 ⊢y=B→ADy=ADB
13 oveq2 ⊢y=B→zDy=zDB
14 13 oveq2d ⊢y=B→zDA+𝑒zDy=zDA+𝑒zDB
15 12 14 breq12d ⊢y=B→ADy≤zDA+𝑒zDy↔ADB≤zDA+𝑒zDB
16 oveq1 ⊢z=C→zDA=CDA
17 oveq1 ⊢z=C→zDB=CDB
18 16 17 oveq12d ⊢z=C→zDA+𝑒zDB=CDA+𝑒CDB
19 18 breq2d ⊢z=C→ADB≤zDA+𝑒zDB↔ADB≤CDA+𝑒CDB
20 11 15 19 rspc3v ⊢A∈X∧B∈X∧C∈X→∀x∈X∀y∈X∀z∈XxDy≤zDx+𝑒zDy→ADB≤CDA+𝑒CDB
21 7 20 syl5 ⊢A∈X∧B∈X∧C∈X→D∈∞Met⁡X→ADB≤CDA+𝑒CDB
22 21 3comr ⊢C∈X∧A∈X∧B∈X→D∈∞Met⁡X→ADB≤CDA+𝑒CDB
23 22 impcom ⊢D∈∞Met⁡X∧C∈X∧A∈X∧B∈X→ADB≤CDA+𝑒CDB