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

Metamath Proof Explorer

Definition df-met

Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms . However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of Gleason p. 223. The 4 properties in Gleason's definition are shown by met0 , metgt0 , metsym , and mettri . (Contributed by NM, 25-Aug-2006)

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

Detailed syntax breakdown

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