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⇝vA↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x

Proof

Step Hyp Ref Expression
1 breq2 ⊢w=A→F⇝vw↔F⇝vA
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∈ℤ≥ynormℎ⁡F⁡z-ℎw<x↔∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
6 5 ralbidv ⊢w=A→∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎw<x↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
7 1 6 bibi12d ⊢w=A→F⇝vw↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎw<x↔F⇝vA↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
8 7 imbi2d ⊢w=A→F:ℕ⟶ℋ→F⇝vw↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎw<x↔F:ℕ⟶ℋ→F⇝vA↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
9 vex ⊢w∈V
10 9 hlimi ⊢F⇝vw↔F:ℕ⟶ℋ∧w∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎw<x
11 10 baib ⊢F:ℕ⟶ℋ∧w∈ℋ→F⇝vw↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎw<x
12 11 expcom ⊢w∈ℋ→F:ℕ⟶ℋ→F⇝vw↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎw<x
13 8 12 vtoclga ⊢A∈ℋ→F:ℕ⟶ℋ→F⇝vA↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
14 13 impcom ⊢F:ℕ⟶ℋ∧A∈ℋ→F⇝vA↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x