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

Metamath Proof Explorer

Definition df-hcau

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau for its membership relation. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in Beran p. 96. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

Ref Expression
Assertion df-hcau Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccauold ⊢ Cauchy
1 vf ⊢ 𝑓
2 chba ⊢ ℋ
3 cmap ⊢ ↑m
4 cn ⊢ ℕ
5 2 4 3 co ⊢ ( ℋ ↑m ℕ )
6 vx ⊢ 𝑥
7 crp ⊢ ℝ+
8 vy ⊢ 𝑦
9 vz ⊢ 𝑧
10 cuz ⊢ ℤ≥
11 8 cv ⊢ 𝑦
12 11 10 cfv ⊢ ( ℤ≥ ‘ 𝑦 )
13 cno ⊢ normℎ
14 1 cv ⊢ 𝑓
15 11 14 cfv ⊢ ( 𝑓 ‘ 𝑦 )
16 cmv ⊢ −ℎ
17 9 cv ⊢ 𝑧
18 17 14 cfv ⊢ ( 𝑓 ‘ 𝑧 )
19 15 18 16 co ⊢ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) )
20 19 13 cfv ⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) )
21 clt ⊢ <
22 6 cv ⊢ 𝑥
23 20 22 21 wbr ⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
24 23 9 12 wral ⊢ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
25 24 8 4 wrex ⊢ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
26 25 6 7 wral ⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
27 26 1 5 crab ⊢ { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 }
28 0 27 wceq ⊢ Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 }