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

Metamath Proof Explorer

Definition df-hlim

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

Ref Expression
Assertion df-hlim ⇝𝑣 = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 chli ⊢ ⇝𝑣
1 vf ⊢ 𝑓
2 vw ⊢ 𝑤
3 1 cv ⊢ 𝑓
4 cn ⊢ ℕ
5 chba ⊢ ℋ
6 4 5 3 wf ⊢ 𝑓 : ℕ ⟶ ℋ
7 2 cv ⊢ 𝑤
8 7 5 wcel ⊢ 𝑤 ∈ ℋ
9 6 8 wa ⊢ ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ )
10 vx ⊢ 𝑥
11 crp ⊢ ℝ+
12 vy ⊢ 𝑦
13 vz ⊢ 𝑧
14 cuz ⊢ ℤ≥
15 12 cv ⊢ 𝑦
16 15 14 cfv ⊢ ( ℤ≥ ‘ 𝑦 )
17 cno ⊢ normℎ
18 13 cv ⊢ 𝑧
19 18 3 cfv ⊢ ( 𝑓 ‘ 𝑧 )
20 cmv ⊢ −ℎ
21 19 7 20 co ⊢ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 )
22 21 17 cfv ⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) )
23 clt ⊢ <
24 10 cv ⊢ 𝑥
25 22 24 23 wbr ⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥
26 25 13 16 wral ⊢ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥
27 26 12 4 wrex ⊢ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥
28 27 10 11 wral ⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥
29 9 28 wa ⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 )
30 29 1 2 copab ⊢ { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) }
31 0 30 wceq ⊢ ⇝𝑣 = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) }