Metamath Proof Explorer

Theorem ismet2

Description: An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion ismet2 ⊢D∈Met⁡X↔D∈∞Met⁡X∧D:X×X⟶ℝ

Proof

Step Hyp Ref Expression
1 elfvex ⊢D∈Met⁡X→X∈V
2 elfvex ⊢D∈∞Met⁡X→X∈V
3 2 adantr ⊢D∈∞Met⁡X∧D:X×X⟶ℝ→X∈V
4 simpllr ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→D:X×X⟶ℝ
5 simpr ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→z∈X
6 simplrl ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→x∈X
7 4 5 6 fovcdmd ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→zDx∈ℝ
8 simplrr ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→y∈X
9 4 5 8 fovcdmd ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→zDy∈ℝ
10 7 9 rexaddd ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→zDx+𝑒zDy=zDx+zDy
11 10 breq2d ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X∧z∈X→xDy≤zDx+𝑒zDy↔xDy≤zDx+zDy
12 11 ralbidva ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X→∀z∈XxDy≤zDx+𝑒zDy↔∀z∈XxDy≤zDx+zDy
13 12 anbi2d ⊢X∈V∧D:X×X⟶ℝ∧x∈X∧y∈X→xDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy↔xDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
14 13 2ralbidva ⊢X∈V∧D:X×X⟶ℝ→∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy↔∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
15 simpr ⊢X∈V∧D:X×X⟶ℝ→D:X×X⟶ℝ
16 ressxr ⊢ℝ⊆ℝ*
17 fss ⊢D:X×X⟶ℝ∧ℝ⊆ℝ*→D:X×X⟶ℝ*
18 15 16 17 sylancl ⊢X∈V∧D:X×X⟶ℝ→D:X×X⟶ℝ*
19 18 biantrurd ⊢X∈V∧D:X×X⟶ℝ→∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
20 14 19 bitr3d ⊢X∈V∧D:X×X⟶ℝ→∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
21 20 pm5.32da ⊢X∈V→D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy↔D:X×X⟶ℝ∧D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
22 21 biancomd ⊢X∈V→D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy∧D:X×X⟶ℝ
23 ismet ⊢X∈V→D∈Met⁡X↔D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
24 isxmet ⊢X∈V→D∈∞Met⁡X↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
25 24 anbi1d ⊢X∈V→D∈∞Met⁡X∧D:X×X⟶ℝ↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy∧D:X×X⟶ℝ
26 22 23 25 3bitr4d ⊢X∈V→D∈Met⁡X↔D∈∞Met⁡X∧D:X×X⟶ℝ
27 1 3 26 pm5.21nii ⊢D∈Met⁡X↔D∈∞Met⁡X∧D:X×X⟶ℝ