This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-psmet

Description: Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion df-psmet PsMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsmet ⊢ PsMet
1 vx ⊢ 𝑥
2 cvv ⊢ V
3 vd ⊢ 𝑑
4 cxr ⊢ ℝ*
5 cmap ⊢ ↑m
6 1 cv ⊢ 𝑥
7 6 6 cxp ⊢ ( 𝑥 × 𝑥 )
8 4 7 5 co ⊢ ( ℝ* ↑m ( 𝑥 × 𝑥 ) )
9 vy ⊢ 𝑦
10 9 cv ⊢ 𝑦
11 3 cv ⊢ 𝑑
12 10 10 11 co ⊢ ( 𝑦 𝑑 𝑦 )
13 cc0 ⊢ 0
14 12 13 wceq ⊢ ( 𝑦 𝑑 𝑦 ) = 0
15 vz ⊢ 𝑧
16 vw ⊢ 𝑤
17 15 cv ⊢ 𝑧
18 10 17 11 co ⊢ ( 𝑦 𝑑 𝑧 )
19 cle ⊢ ≤
20 16 cv ⊢ 𝑤
21 20 10 11 co ⊢ ( 𝑤 𝑑 𝑦 )
22 cxad ⊢ +𝑒
23 20 17 11 co ⊢ ( 𝑤 𝑑 𝑧 )
24 21 23 22 co ⊢ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) )
25 18 24 19 wbr ⊢ ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) )
26 25 16 6 wral ⊢ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) )
27 26 15 6 wral ⊢ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) )
28 14 27 wa ⊢ ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) )
29 28 9 6 wral ⊢ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) )
30 29 3 8 crab ⊢ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) }
31 1 2 30 cmpt ⊢ ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) } )
32 0 31 wceq ⊢ PsMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) } )