Metamath Proof Explorer

Theorem ispsmet

Description: Express the predicate " D is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion ispsmet ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y

Proof

Step Hyp Ref Expression
1 elex ⊢ X ∈ V → X ∈ V
2 id ⊢ u = X → u = X
3 2 sqxpeqd ⊢ u = X → u × u = X × X
4 3 oveq2d ⊢ u = X → ℝ * u × u = ℝ * X × X
5 raleq ⊢ u = X → ∀ z ∈ u x d y ≤ z d x + 𝑒 z d y ↔ ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
6 5 raleqbi1dv ⊢ u = X → ∀ y ∈ u ∀ z ∈ u x d y ≤ z d x + 𝑒 z d y ↔ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
7 6 anbi2d ⊢ u = X → x d x = 0 ∧ ∀ y ∈ u ∀ z ∈ u x d y ≤ z d x + 𝑒 z d y ↔ x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
8 7 raleqbi1dv ⊢ u = X → ∀ x ∈ u x d x = 0 ∧ ∀ y ∈ u ∀ z ∈ u x d y ≤ z d x + 𝑒 z d y ↔ ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
9 4 8 rabeqbidv ⊢ u = X → d ∈ ℝ * u × u | ∀ x ∈ u x d x = 0 ∧ ∀ y ∈ u ∀ z ∈ u x d y ≤ z d x + 𝑒 z d y = d ∈ ℝ * X × X | ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
10 df-psmet ⊢ PsMet = u ∈ V ⟼ d ∈ ℝ * u × u | ∀ x ∈ u x d x = 0 ∧ ∀ y ∈ u ∀ z ∈ u x d y ≤ z d x + 𝑒 z d y
11 ovex ⊢ ℝ * X × X ∈ V
12 11 rabex ⊢ d ∈ ℝ * X × X | ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y ∈ V
13 9 10 12 fvmpt ⊢ X ∈ V → PsMet ⁡ X = d ∈ ℝ * X × X | ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
14 1 13 syl ⊢ X ∈ V → PsMet ⁡ X = d ∈ ℝ * X × X | ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
15 14 eleq2d ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D ∈ d ∈ ℝ * X × X | ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y
16 oveq ⊢ d = D → x d x = x D x
17 16 eqeq1d ⊢ d = D → x d x = 0 ↔ x D x = 0
18 oveq ⊢ d = D → x d y = x D y
19 oveq ⊢ d = D → z d x = z D x
20 oveq ⊢ d = D → z d y = z D y
21 19 20 oveq12d ⊢ d = D → z d x + 𝑒 z d y = z D x + 𝑒 z D y
22 18 21 breq12d ⊢ d = D → x d y ≤ z d x + 𝑒 z d y ↔ x D y ≤ z D x + 𝑒 z D y
23 22 2ralbidv ⊢ d = D → ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y ↔ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
24 17 23 anbi12d ⊢ d = D → x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y ↔ x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
25 24 ralbidv ⊢ d = D → ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y ↔ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
26 25 elrab ⊢ D ∈ d ∈ ℝ * X × X | ∀ x ∈ X x d x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x d y ≤ z d x + 𝑒 z d y ↔ D ∈ ℝ * X × X ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
27 15 26 syl6bb ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D ∈ ℝ * X × X ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
28 xrex ⊢ ℝ * ∈ V
29 sqxpexg ⊢ X ∈ V → X × X ∈ V
30 elmapg ⊢ ℝ * ∈ V ∧ X × X ∈ V → D ∈ ℝ * X × X ↔ D : X × X ⟶ ℝ *
31 28 29 30 sylancr ⊢ X ∈ V → D ∈ ℝ * X × X ↔ D : X × X ⟶ ℝ *
32 31 anbi1d ⊢ X ∈ V → D ∈ ℝ * X × X ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
33 27 32 bitrd ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y