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

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ℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )