Metamath Proof Explorer


Theorem hlim2

Description: The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlim2 ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐹𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝑤 = 𝐴 → ( 𝐹𝑣 𝑤𝐹𝑣 𝐴 ) )
2 oveq2 ( 𝑤 = 𝐴 → ( ( 𝐹𝑧 ) − 𝑤 ) = ( ( 𝐹𝑧 ) − 𝐴 ) )
3 2 fveq2d ( 𝑤 = 𝐴 → ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) = ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) )
4 3 breq1d ( 𝑤 = 𝐴 → ( ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ↔ ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) )
5 4 rexralbidv ( 𝑤 = 𝐴 → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) )
6 5 ralbidv ( 𝑤 = 𝐴 → ( ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) )
7 1 6 bibi12d ( 𝑤 = 𝐴 → ( ( 𝐹𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ( 𝐹𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) ) )
8 7 imbi2d ( 𝑤 = 𝐴 → ( ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ) ) ↔ ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) ) ) )
9 vex 𝑤 ∈ V
10 9 hlimi ( 𝐹𝑣 𝑤 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ) )
11 10 baib ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝐹𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ) )
12 11 expcom ( 𝑤 ∈ ℋ → ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹𝑣 𝑤 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝑤 ) ) < 𝑥 ) ) )
13 8 12 vtoclga ( 𝐴 ∈ ℋ → ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) ) )
14 13 impcom ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐹𝑣 𝐴 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 𝑥 ) )