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 \in V$
	Assertion	hlimi	$⊢ F \underset{v}{⇝} A \leftrightarrow ((F : ℕ ⟶ ℋ \land A \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x)$

Proof

Step	Hyp	Ref	Expression
1		hlim.1	$⊢ A \in V$
2		df-hlim	$⊢ \underset{v}{⇝} = \{⟨f, w⟩ \| ((f : ℕ ⟶ ℋ \land w \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (f (z) -_{ℎ} w) < x)\}$
3	2	relopabiv	$⊢ Rel \underset{v}{⇝}$
4	3	brrelex1i	$⊢ F \underset{v}{⇝} A \to F \in V$
5		nnex	$⊢ ℕ \in V$
6		fex	$⊢ (F : ℕ ⟶ ℋ \land ℕ \in V) \to F \in V$
7	5 6	mpan2	$⊢ F : ℕ ⟶ ℋ \to F \in V$
8	7	ad2antrr	$⊢ ((F : ℕ ⟶ ℋ \land A \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x) \to F \in V$
9		feq1	$⊢ f = F \to (f : ℕ ⟶ ℋ \leftrightarrow F : ℕ ⟶ ℋ)$
10		eleq1	$⊢ w = A \to (w \in ℋ \leftrightarrow A \in ℋ)$
11	9 10	bi2anan9	$⊢ (f = F \land w = A) \to ((f : ℕ ⟶ ℋ \land w \in ℋ) \leftrightarrow (F : ℕ ⟶ ℋ \land A \in ℋ))$
12		fveq1	$⊢ f = F \to f (z) = F (z)$
13		oveq12	$⊢ (f (z) = F (z) \land w = A) \to f (z) -_{ℎ} w = F (z) -_{ℎ} A$
14	12 13	sylan	$⊢ (f = F \land w = A) \to f (z) -_{ℎ} w = F (z) -_{ℎ} A$
15	14	fveq2d	$⊢ (f = F \land w = A) \to {norm}_{ℎ} (f (z) -_{ℎ} w) = {norm}_{ℎ} (F (z) -_{ℎ} A)$
16	15	breq1d	$⊢ (f = F \land w = A) \to ({norm}_{ℎ} (f (z) -_{ℎ} w) < x \leftrightarrow {norm}_{ℎ} (F (z) -_{ℎ} A) < x)$
17	16	rexralbidv	$⊢ (f = F \land w = A) \to (\exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (f (z) -_{ℎ} w) < x \leftrightarrow \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x)$
18	17	ralbidv	$⊢ (f = F \land w = A) \to (\forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (f (z) -_{ℎ} w) < x \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x)$
19	11 18	anbi12d	$⊢ (f = F \land w = A) \to (((f : ℕ ⟶ ℋ \land w \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (f (z) -_{ℎ} w) < x) \leftrightarrow ((F : ℕ ⟶ ℋ \land A \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x))$
20	19 2	brabga	$⊢ (F \in V \land A \in V) \to (F \underset{v}{⇝} A \leftrightarrow ((F : ℕ ⟶ ℋ \land A \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x))$
21	1 20	mpan2	$⊢ F \in V \to (F \underset{v}{⇝} A \leftrightarrow ((F : ℕ ⟶ ℋ \land A \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x))$
22	4 8 21	pm5.21nii	$⊢ F \underset{v}{⇝} A \leftrightarrow ((F : ℕ ⟶ ℋ \land A \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x)$

Metamath Proof Explorer

Theorem hlimi

Proof