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 ⊢ F : ℕ ⟶ ℋ ∧ A ∈ ℋ → F ⇝v A ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x

Proof

Step Hyp Ref Expression
1 breq2 ⊢ w = A → F ⇝v w ↔ F ⇝v A
2 oveq2 ⊢ w = A → F ⁡ z - ℎ w = F ⁡ z - ℎ A
3 2 fveq2d ⊢ w = A → norm ℎ ⁡ F ⁡ z - ℎ w = norm ℎ ⁡ F ⁡ z - ℎ A
4 3 breq1d ⊢ w = A → norm ℎ ⁡ F ⁡ z - ℎ w < x ↔ norm ℎ ⁡ F ⁡ z - ℎ A < x
5 4 rexralbidv ⊢ w = A → ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ w < x ↔ ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x
6 5 ralbidv ⊢ w = A → ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ w < x ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x
7 1 6 bibi12d ⊢ w = A → F ⇝v w ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ w < x ↔ F ⇝v A ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x
8 7 imbi2d ⊢ w = A → F : ℕ ⟶ ℋ → F ⇝v w ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ w < x ↔ F : ℕ ⟶ ℋ → F ⇝v A ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x
9 vex ⊢ w ∈ V
10 9 hlimi ⊢ F ⇝v w ↔ F : ℕ ⟶ ℋ ∧ w ∈ ℋ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ w < x
11 10 baib ⊢ F : ℕ ⟶ ℋ ∧ w ∈ ℋ → F ⇝v w ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ w < x
12 11 expcom ⊢ w ∈ ℋ → F : ℕ ⟶ ℋ → F ⇝v w ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ w < x
13 8 12 vtoclga ⊢ A ∈ ℋ → F : ℕ ⟶ ℋ → F ⇝v A ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x
14 13 impcom ⊢ F : ℕ ⟶ ℋ ∧ A ∈ ℋ → F ⇝v A ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x