Metamath Proof Explorer


Theorem ispsmet

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

Ref Expression
Assertion ispsmet ( 𝑋𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elex ( 𝑋𝑉𝑋 ∈ V )
2 id ( 𝑢 = 𝑋𝑢 = 𝑋 )
3 2 sqxpeqd ( 𝑢 = 𝑋 → ( 𝑢 × 𝑢 ) = ( 𝑋 × 𝑋 ) )
4 3 oveq2d ( 𝑢 = 𝑋 → ( ℝ*m ( 𝑢 × 𝑢 ) ) = ( ℝ*m ( 𝑋 × 𝑋 ) ) )
5 raleq ( 𝑢 = 𝑋 → ( ∀ 𝑧𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) )
6 5 raleqbi1dv ( 𝑢 = 𝑋 → ( ∀ 𝑦𝑢𝑧𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) )
7 6 anbi2d ( 𝑢 = 𝑋 → ( ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑢𝑧𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
8 7 raleqbi1dv ( 𝑢 = 𝑋 → ( ∀ 𝑥𝑢 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑢𝑧𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
9 4 8 rabeqbidv ( 𝑢 = 𝑋 → { 𝑑 ∈ ( ℝ*m ( 𝑢 × 𝑢 ) ) ∣ ∀ 𝑥𝑢 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑢𝑧𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } = { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
10 df-psmet PsMet = ( 𝑢 ∈ V ↦ { 𝑑 ∈ ( ℝ*m ( 𝑢 × 𝑢 ) ) ∣ ∀ 𝑥𝑢 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑢𝑧𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
11 ovex ( ℝ*m ( 𝑋 × 𝑋 ) ) ∈ V
12 11 rabex { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ∈ V
13 9 10 12 fvmpt ( 𝑋 ∈ V → ( PsMet ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
14 1 13 syl ( 𝑋𝑉 → ( PsMet ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
15 14 eleq2d ( 𝑋𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ 𝐷 ∈ { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ) )
16 oveq ( 𝑑 = 𝐷 → ( 𝑥 𝑑 𝑥 ) = ( 𝑥 𝐷 𝑥 ) )
17 16 eqeq1d ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑥 ) = 0 ↔ ( 𝑥 𝐷 𝑥 ) = 0 ) )
18 oveq ( 𝑑 = 𝐷 → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
19 oveq ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑥 ) = ( 𝑧 𝐷 𝑥 ) )
20 oveq ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑦 ) = ( 𝑧 𝐷 𝑦 ) )
21 19 20 oveq12d ( 𝑑 = 𝐷 → ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
22 18 21 breq12d ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
23 22 2ralbidv ( 𝑑 = 𝐷 → ( ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
24 17 23 anbi12d ( 𝑑 = 𝐷 → ( ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
25 24 ralbidv ( 𝑑 = 𝐷 → ( ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
26 25 elrab ( 𝐷 ∈ { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ↔ ( 𝐷 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
27 15 26 bitrdi ( 𝑋𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
28 xrex * ∈ V
29 sqxpexg ( 𝑋𝑉 → ( 𝑋 × 𝑋 ) ∈ V )
30 elmapg ( ( ℝ* ∈ V ∧ ( 𝑋 × 𝑋 ) ∈ V ) → ( 𝐷 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ↔ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ) )
31 28 29 30 sylancr ( 𝑋𝑉 → ( 𝐷 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ↔ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ) )
32 31 anbi1d ( 𝑋𝑉 → ( ( 𝐷 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
33 27 32 bitrd ( 𝑋𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )