Theorem hlimadd

Description: Limit of the sum of two sequences in a Hilbert vector space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlimadd.3	$$⊢\phi \to F:\mathbb{N}⟶\mathscr{H}$$
	hlimadd.4	$$⊢\phi \to G:\mathbb{N}⟶\mathscr{H}$$
	hlimadd.5	$$⊢\phi \to F\underset{v}{⇝}A$$
	hlimadd.6	$$⊢\phi \to G\underset{v}{⇝}B$$
	hlimadd.7	$$⊢H=\left(n\in \mathbb{N}⟼F\left(n\right){+}_{ℎ}G\left(n\right)\right)$$
Assertion	hlimadd	$$⊢\phi \to H\underset{v}{⇝}\left(A{+}_{ℎ}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlimadd.3	$$⊢\phi \to F:\mathbb{N}⟶\mathscr{H}$$
2		hlimadd.4	$$⊢\phi \to G:\mathbb{N}⟶\mathscr{H}$$
3		hlimadd.5	$$⊢\phi \to F\underset{v}{⇝}A$$
4		hlimadd.6	$$⊢\phi \to G\underset{v}{⇝}B$$
5		hlimadd.7	$$⊢H=\left(n\in \mathbb{N}⟼F\left(n\right){+}_{ℎ}G\left(n\right)\right)$$
6	1	ffvelcdmda	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to F\left(n\right)\in \mathscr{H}$$
7	2	ffvelcdmda	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to G\left(n\right)\in \mathscr{H}$$
8		hvaddcl	$$⊢\left(F\left(n\right)\in \mathscr{H}\wedge G\left(n\right)\in \mathscr{H}\right)\to F\left(n\right){+}_{ℎ}G\left(n\right)\in \mathscr{H}$$
9	6 7 8	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to F\left(n\right){+}_{ℎ}G\left(n\right)\in \mathscr{H}$$
10	9 5	fmptd	$$⊢\phi \to H:\mathbb{N}⟶\mathscr{H}$$
11		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
12		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
13	11 12	elmap	$$⊢H\in \left({\mathscr{H}}^{\mathbb{N}}\right)\leftrightarrow H:\mathbb{N}⟶\mathscr{H}$$
14	10 13	sylibr	$$⊢\phi \to H\in \left({\mathscr{H}}^{\mathbb{N}}\right)$$
15		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
16		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
17		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
18		eqid	$$⊢{norm}_{ℎ}\circ {-}_{ℎ}={norm}_{ℎ}\circ {-}_{ℎ}$$
19	17 18	hhims	$$⊢{norm}_{ℎ}\circ {-}_{ℎ}=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
20	17 19	hhxmet	$$⊢{norm}_{ℎ}\circ {-}_{ℎ}\in \mathrm{\infty Met}\left(\mathscr{H}\right)$$
21		eqid	$$⊢\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)=\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)$$
22	21	mopntopon	$$⊢{norm}_{ℎ}\circ {-}_{ℎ}\in \mathrm{\infty Met}\left(\mathscr{H}\right)\to \mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)$$
23	20 22	mp1i	$$⊢\phi \to \mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)$$
24	17	hhnv	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$$
25		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
26	17 24 25 19 21	h2hlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$
27		resss	$$⊢{\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\subseteq \underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)$$
28	26 27	eqsstri	$$⊢\underset{v}{⇝}\subseteq \underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)$$
29	28	ssbri	$$⊢F\underset{v}{⇝}A\to F\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)A$$
30	3 29	syl	$$⊢\phi \to F\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)A$$
31	28	ssbri	$$⊢G\underset{v}{⇝}B\to G\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)B$$
32	4 31	syl	$$⊢\phi \to G\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)B$$
33	17	hhva	$$⊢{+}_{ℎ}={+}_v\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
34	19 21 33	vacn	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}\to {+}_{ℎ}\in \left(\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right){\times }_t\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\mathrm{Cn}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)$$
35	24 34	mp1i	$$⊢\phi \to {+}_{ℎ}\in \left(\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right){\times }_t\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\mathrm{Cn}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)$$
36	15 16 23 23 1 2 30 32 35 5	lmcn2	$$⊢\phi \to H\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\left(A{+}_{ℎ}B\right)$$
37	26	breqi	$$⊢H\underset{v}{⇝}\left(A{+}_{ℎ}B\right)\leftrightarrow H\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)\left(A{+}_{ℎ}B\right)$$
38		ovex	$$⊢A{+}_{ℎ}B\in \mathrm{V}$$
39	38	brresi	$$⊢H\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)\left(A{+}_{ℎ}B\right)\leftrightarrow \left(H\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge H\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\left(A{+}_{ℎ}B\right)\right)$$
40	37 39	bitri	$$⊢H\underset{v}{⇝}\left(A{+}_{ℎ}B\right)\leftrightarrow \left(H\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge H\underset{t}{⇝}\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\left(A{+}_{ℎ}B\right)\right)$$
41	14 36 40	sylanbrc	$$⊢\phi \to H\underset{v}{⇝}\left(A{+}_{ℎ}B\right)$$