Metamath Proof Explorer

Theorem hlimi

Description: Express the predicate: The limit of vector sequence F in a Hilbert space is A , i.e. F converges to A . This means that for any real x , no matter how small, there always exists an integer y such that the norm of any later vector in the sequence minus the limit is less than x . Definition of converge in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis hlim.1 ⊢A∈V
Assertion hlimi ⊢F⇝vA↔F:ℕ⟶ℋ∧A∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x

Proof

Step Hyp Ref Expression
1 hlim.1 ⊢A∈V
2 df-hlim ⊢⇝v=fw|f:ℕ⟶ℋ∧w∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x
3 2 relopabiv ⊢Rel⁡⇝v
4 3 brrelex1i ⊢F⇝vA→F∈V
5 nnex ⊢ℕ∈V
6 fex ⊢F:ℕ⟶ℋ∧ℕ∈V→F∈V
7 5 6 mpan2 ⊢F:ℕ⟶ℋ→F∈V
8 7 ad2antrr ⊢F:ℕ⟶ℋ∧A∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x→F∈V
9 feq1 ⊢f=F→f:ℕ⟶ℋ↔F:ℕ⟶ℋ
10 eleq1 ⊢w=A→w∈ℋ↔A∈ℋ
11 9 10 bi2anan9 ⊢f=F∧w=A→f:ℕ⟶ℋ∧w∈ℋ↔F:ℕ⟶ℋ∧A∈ℋ
12 fveq1 ⊢f=F→f⁡z=F⁡z
13 oveq12 ⊢f⁡z=F⁡z∧w=A→f⁡z-ℎw=F⁡z-ℎA
14 12 13 sylan ⊢f=F∧w=A→f⁡z-ℎw=F⁡z-ℎA
15 14 fveq2d ⊢f=F∧w=A→normℎ⁡f⁡z-ℎw=normℎ⁡F⁡z-ℎA
16 15 breq1d ⊢f=F∧w=A→normℎ⁡f⁡z-ℎw<x↔normℎ⁡F⁡z-ℎA<x
17 16 rexralbidv ⊢f=F∧w=A→∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x↔∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
18 17 ralbidv ⊢f=F∧w=A→∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x↔∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
19 11 18 anbi12d ⊢f=F∧w=A→f:ℕ⟶ℋ∧w∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x↔F:ℕ⟶ℋ∧A∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
20 19 2 brabga ⊢F∈V∧A∈V→F⇝vA↔F:ℕ⟶ℋ∧A∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
21 1 20 mpan2 ⊢F∈V→F⇝vA↔F:ℕ⟶ℋ∧A∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x
22 4 8 21 pm5.21nii ⊢F⇝vA↔F:ℕ⟶ℋ∧A∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡F⁡z-ℎA<x