Theorem hlim0

Description: The zero sequence in Hilbert space converges to the zero vector. (Contributed by NM, 17-Aug-1999) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hlim0	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{v}{⇝}{0}_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2	1	fconst6	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right):\mathbb{N}⟶\mathscr{H}$$
3		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
4		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
5	3 4	elmap	$$⊢\mathbb{N}\times \left\{0_{ℎ}\right\}\in \left({\mathscr{H}}^{\mathbb{N}}\right)\leftrightarrow \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right):\mathbb{N}⟶\mathscr{H}$$
6	2 5	mpbir	$$⊢\mathbb{N}\times \left\{0_{ℎ}\right\}\in \left({\mathscr{H}}^{\mathbb{N}}\right)$$
7		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
8		eqid	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
9	7 8	hhxmet	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)$$
10		eqid	$$⊢\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)=\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)$$
11	10	mopntopon	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)\to \mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)$$
12	9 11	ax-mp	$$⊢\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)$$
13		1z	$$⊢1\in \mathbb{Z}$$
14		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
15	14	lmconst	$$⊢\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)\wedge 0_{ℎ}\in \mathscr{H}\wedge 1\in \mathbb{Z}\right)\to \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)0_{ℎ}$$
16	12 1 13 15	mp3an	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)0_{ℎ}$$
17	7 8 10	hhlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$
18	17	breqi	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{v}{⇝}{0}_{ℎ}\leftrightarrow \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)0_{ℎ}$$
19	1	elexi	$$⊢0_{ℎ}\in \mathrm{V}$$
20	19	brresi	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)0_{ℎ}\leftrightarrow \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)0_{ℎ}\right)$$
21	18 20	bitri	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{v}{⇝}{0}_{ℎ}\leftrightarrow \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)0_{ℎ}\right)$$
22	6 16 21	mpbir2an	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{v}{⇝}{0}_{ℎ}$$