Theorem hlimcaui

Description: If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. (Contributed by NM, 17-Aug-1999) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hlimcaui	$$⊢F\underset{v}{⇝}A\to F\in \mathrm{Cauchy}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		eqid	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
3		eqid	$$⊢\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)=\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)$$
4	1 2 3	hhlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$
5		resss	$$⊢{\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\subseteq \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
6	4 5	eqsstri	$$⊢\underset{v}{⇝}\subseteq \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
7		dmss	$$⊢\underset{v}{⇝}\subseteq \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\to \mathrm{dom}\underset{v}{⇝}\subseteq \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
8	6 7	ax-mp	$$⊢\mathrm{dom}\underset{v}{⇝}\subseteq \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
9	1 2	hhxmet	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)$$
10	3	lmcau	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)\to \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\subseteq \mathrm{Cau}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)$$
11	9 10	ax-mp	$$⊢\mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\subseteq \mathrm{Cau}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)$$
12	8 11	sstri	$$⊢\mathrm{dom}\underset{v}{⇝}\subseteq \mathrm{Cau}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)$$
13	4	dmeqi	$$⊢\mathrm{dom}\underset{v}{⇝}=\mathrm{dom}\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)$$
14		dmres	$$⊢\mathrm{dom}\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)=\left({\mathscr{H}}^{\mathbb{N}}\right)\cap \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
15	13 14	eqtri	$$⊢\mathrm{dom}\underset{v}{⇝}=\left({\mathscr{H}}^{\mathbb{N}}\right)\cap \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
16		inss1	$$⊢\left({\mathscr{H}}^{\mathbb{N}}\right)\cap \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\subseteq {\mathscr{H}}^{\mathbb{N}}$$
17	15 16	eqsstri	$$⊢\mathrm{dom}\underset{v}{⇝}\subseteq {\mathscr{H}}^{\mathbb{N}}$$
18	12 17	ssini	$$⊢\mathrm{dom}\underset{v}{⇝}\subseteq \mathrm{Cau}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)$$
19	1 2	hhcau	$$⊢\mathrm{Cauchy}=\mathrm{Cau}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)$$
20	18 19	sseqtrri	$$⊢\mathrm{dom}\underset{v}{⇝}\subseteq \mathrm{Cauchy}$$
21		relres	$$⊢\mathrm{Rel}\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)$$
22	4	releqi	$$⊢\mathrm{Rel}\underset{v}{⇝}\leftrightarrow \mathrm{Rel}\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)$$
23	21 22	mpbir	$$⊢\mathrm{Rel}\underset{v}{⇝}$$
24	23	releldmi	$$⊢F\underset{v}{⇝}A\to F\in \mathrm{dom}\underset{v}{⇝}$$
25	20 24	sseldi	$$⊢F\underset{v}{⇝}A\to F\in \mathrm{Cauchy}$$