h2hlm

Description: The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2hl.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
	h2hl.2	$⊢ U \in NrmCVec$
	h2hl.3	$⊢ ℋ = BaseSet (U)$
	h2hl.4	$⊢ D = IndMet (U)$
	h2hl.5	$⊢ J = MetOpen (D)$
Assertion	h2hlm	$⊢ \underset{v}{⇝} = {\underset{t}{⇝} (J) ↾}_{(ℋ^{ℕ})}$

Proof

Step	Hyp	Ref	Expression
1		h2hl.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2		h2hl.2	$⊢ U \in NrmCVec$
3		h2hl.3	$⊢ ℋ = BaseSet (U)$
4		h2hl.4	$⊢ D = IndMet (U)$
5		h2hl.5	$⊢ J = MetOpen (D)$
6		df-hlim	$⊢ \underset{v}{⇝} = \{⟨f, x⟩ \| ((f : ℕ ⟶ ℋ \land x \in ℋ) \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)\}$
7	6	relopabiv	$⊢ Rel \underset{v}{⇝}$
8		relres	$⊢ Rel ({\underset{t}{⇝} (J) ↾}_{(ℋ^{ℕ})})$
9	6	eleq2i	$⊢ ⟨f, x⟩ \in \underset{v}{⇝} \leftrightarrow ⟨f, x⟩ \in \{⟨f, x⟩ \| ((f : ℕ ⟶ ℋ \land x \in ℋ) \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)\}$
10		opabidw	$⊢ ⟨f, x⟩ \in \{⟨f, x⟩ \| ((f : ℕ ⟶ ℋ \land x \in ℋ) \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)\} \leftrightarrow ((f : ℕ ⟶ ℋ \land x \in ℋ) \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
11	3	hlex	$⊢ ℋ \in V$
12		nnex	$⊢ ℕ \in V$
13	11 12	elmap	$⊢ f \in (ℋ^{ℕ}) \leftrightarrow f : ℕ ⟶ ℋ$
14	13	anbi1i	$⊢ (f \in (ℋ^{ℕ}) \land ⟨f, x⟩ \in \underset{t}{⇝} (J)) \leftrightarrow (f : ℕ ⟶ ℋ \land ⟨f, x⟩ \in \underset{t}{⇝} (J))$
15		df-br	$⊢ f \underset{t}{⇝} (J) x \leftrightarrow ⟨f, x⟩ \in \underset{t}{⇝} (J)$
16	3 4	imsxmet	$⊢ U \in NrmCVec \to D \in ∞Met (ℋ)$
17	2 16	mp1i	$⊢ f : ℕ ⟶ ℋ \to D \in ∞Met (ℋ)$
18		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
19		1zzd	$⊢ f : ℕ ⟶ ℋ \to 1 \in ℤ$
20		eqidd	$⊢ (f : ℕ ⟶ ℋ \land k \in ℕ) \to f (k) = f (k)$
21		id	$⊢ f : ℕ ⟶ ℋ \to f : ℕ ⟶ ℋ$
22	5 17 18 19 20 21	lmmbrf	$⊢ f : ℕ ⟶ ℋ \to (f \underset{t}{⇝} (J) x \leftrightarrow (x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} f (k) D x < y))$
23		eluznn	$⊢ (j \in ℕ \land k \in ℤ_{\geq j}) \to k \in ℕ$
24		ffvelcdm	$⊢ (f : ℕ ⟶ ℋ \land k \in ℕ) \to f (k) \in ℋ$
25	1 2 3 4	h2hmetdval	$⊢ (f (k) \in ℋ \land x \in ℋ) \to f (k) D x = {norm}_{ℎ} (f (k) -_{ℎ} x)$
26	24 25	sylan	$⊢ ((f : ℕ ⟶ ℋ \land k \in ℕ) \land x \in ℋ) \to f (k) D x = {norm}_{ℎ} (f (k) -_{ℎ} x)$
27	26	breq1d	$⊢ ((f : ℕ ⟶ ℋ \land k \in ℕ) \land x \in ℋ) \to (f (k) D x < y \leftrightarrow {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
28	27	an32s	$⊢ ((f : ℕ ⟶ ℋ \land x \in ℋ) \land k \in ℕ) \to (f (k) D x < y \leftrightarrow {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
29	23 28	sylan2	$⊢ ((f : ℕ ⟶ ℋ \land x \in ℋ) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to (f (k) D x < y \leftrightarrow {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
30	29	anassrs	$⊢ (((f : ℕ ⟶ ℋ \land x \in ℋ) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (f (k) D x < y \leftrightarrow {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
31	30	ralbidva	$⊢ ((f : ℕ ⟶ ℋ \land x \in ℋ) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} f (k) D x < y \leftrightarrow \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
32	31	rexbidva	$⊢ (f : ℕ ⟶ ℋ \land x \in ℋ) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} f (k) D x < y \leftrightarrow \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
33	32	ralbidv	$⊢ (f : ℕ ⟶ ℋ \land x \in ℋ) \to (\forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} f (k) D x < y \leftrightarrow \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)$
34	33	pm5.32da	$⊢ f : ℕ ⟶ ℋ \to ((x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} f (k) D x < y) \leftrightarrow (x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y))$
35	22 34	bitrd	$⊢ f : ℕ ⟶ ℋ \to (f \underset{t}{⇝} (J) x \leftrightarrow (x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y))$
36	15 35	bitr3id	$⊢ f : ℕ ⟶ ℋ \to (⟨f, x⟩ \in \underset{t}{⇝} (J) \leftrightarrow (x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y))$
37	36	pm5.32i	$⊢ (f : ℕ ⟶ ℋ \land ⟨f, x⟩ \in \underset{t}{⇝} (J)) \leftrightarrow (f : ℕ ⟶ ℋ \land (x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y))$
38	14 37	bitr2i	$⊢ (f : ℕ ⟶ ℋ \land (x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y)) \leftrightarrow (f \in (ℋ^{ℕ}) \land ⟨f, x⟩ \in \underset{t}{⇝} (J))$
39		anass	$⊢ ((f : ℕ ⟶ ℋ \land x \in ℋ) \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y) \leftrightarrow (f : ℕ ⟶ ℋ \land (x \in ℋ \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y))$
40		opelres	$⊢ x \in V \to (⟨f, x⟩ \in ({\underset{t}{⇝} (J) ↾}_{(ℋ^{ℕ})}) \leftrightarrow (f \in (ℋ^{ℕ}) \land ⟨f, x⟩ \in \underset{t}{⇝} (J)))$
41	40	elv	$⊢ ⟨f, x⟩ \in ({\underset{t}{⇝} (J) ↾}_{(ℋ^{ℕ})}) \leftrightarrow (f \in (ℋ^{ℕ}) \land ⟨f, x⟩ \in \underset{t}{⇝} (J))$
42	38 39 41	3bitr4i	$⊢ ((f : ℕ ⟶ ℋ \land x \in ℋ) \land \forall y \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (k) -_{ℎ} x) < y) \leftrightarrow ⟨f, x⟩ \in ({\underset{t}{⇝} (J) ↾}_{(ℋ^{ℕ})})$
43	9 10 42	3bitri	$⊢ ⟨f, x⟩ \in \underset{v}{⇝} \leftrightarrow ⟨f, x⟩ \in ({\underset{t}{⇝} (J) ↾}_{(ℋ^{ℕ})})$
44	7 8 43	eqrelriiv	$⊢ \underset{v}{⇝} = {\underset{t}{⇝} (J) ↾}_{(ℋ^{ℕ})}$

Metamath Proof Explorer

Theorem h2hlm

Proof