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

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 ⊢ 𝐴 ∈ V
Assertion hlimi ( 𝐹 ⇝𝑣 𝐴 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 hlim.1 ⊢ 𝐴 ∈ V
2 df-hlim ⊢ ⇝𝑣 = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) }
3 2 relopabiv ⊢ Rel ⇝𝑣
4 3 brrelex1i ⊢ ( 𝐹 ⇝𝑣 𝐴 → 𝐹 ∈ V )
5 nnex ⊢ ℕ ∈ V
6 fex ⊢ ( ( 𝐹 : ℕ ⟶ ℋ ∧ ℕ ∈ V ) → 𝐹 ∈ V )
7 5 6 mpan2 ⊢ ( 𝐹 : ℕ ⟶ ℋ → 𝐹 ∈ V )
8 7 ad2antrr ⊢ ( ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) → 𝐹 ∈ V )
9 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ℕ ⟶ ℋ ↔ 𝐹 : ℕ ⟶ ℋ ) )
10 eleq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ∈ ℋ ↔ 𝐴 ∈ ℋ ) )
11 9 10 bi2anan9 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐴 ) → ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ) )
12 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
13 oveq12 ⊢ ( ( ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) = ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) )
14 12 13 sylan ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐴 ) → ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) = ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) )
15 14 fveq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐴 ) → ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) = ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) )
16 15 breq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐴 ) → ( ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ↔ ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )
17 16 rexralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐴 ) → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )
18 17 ralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐴 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )
19 11 18 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐴 ) → ( ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) ) )
20 19 2 brabga ⊢ ( ( 𝐹 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐹 ⇝𝑣 𝐴 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) ) )
21 1 20 mpan2 ⊢ ( 𝐹 ∈ V → ( 𝐹 ⇝𝑣 𝐴 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) ) )
22 4 8 21 pm5.21nii ⊢ ( 𝐹 ⇝𝑣 𝐴 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )