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