Metamath Proof Explorer

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 
|- ( ph -> F : NN --> ~H )
hlimadd.4 
|- ( ph -> G : NN --> ~H )
hlimadd.5 
|- ( ph -> F ~~>v A )
hlimadd.6 
|- ( ph -> G ~~>v B )
hlimadd.7 
|- H = ( n e. NN |-> ( ( F ` n ) +h ( G ` n ) ) )
Assertion hlimadd 
|- ( ph -> H ~~>v ( A +h B ) )

Proof

Step Hyp Ref Expression
1 hlimadd.3 
 |-  ( ph -> F : NN --> ~H )
2 hlimadd.4 
 |-  ( ph -> G : NN --> ~H )
3 hlimadd.5 
 |-  ( ph -> F ~~>v A )
4 hlimadd.6 
 |-  ( ph -> G ~~>v B )
5 hlimadd.7 
 |-  H = ( n e. NN |-> ( ( F ` n ) +h ( G ` n ) ) )
6 1 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. ~H )
7 2 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. ~H )
8 hvaddcl 
 |-  ( ( ( F ` n ) e. ~H /\ ( G ` n ) e. ~H ) -> ( ( F ` n ) +h ( G ` n ) ) e. ~H )
9 6 7 8 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) +h ( G ` n ) ) e. ~H )
10 9 5 fmptd 
 |-  ( ph -> H : NN --> ~H )
11 ax-hilex 
 |-  ~H e. _V
12 nnex 
 |-  NN e. _V
13 11 12 elmap 
 |-  ( H e. ( ~H ^m NN ) <-> H : NN --> ~H )
14 10 13 sylibr 
 |-  ( ph -> H e. ( ~H ^m NN ) )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 1zzd 
 |-  ( ph -> 1 e. ZZ )
17 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
18 eqid 
 |-  ( normh o. -h ) = ( normh o. -h )
19 17 18 hhims 
 |-  ( normh o. -h ) = ( IndMet ` <. <. +h , .h >. , normh >. )
20 17 19 hhxmet 
 |-  ( normh o. -h ) e. ( *Met ` ~H )
21 eqid 
 |-  ( MetOpen ` ( normh o. -h ) ) = ( MetOpen ` ( normh o. -h ) )
22 21 mopntopon 
 |-  ( ( normh o. -h ) e. ( *Met ` ~H ) -> ( MetOpen ` ( normh o. -h ) ) e. ( TopOn ` ~H ) )
23 20 22 mp1i 
 |-  ( ph -> ( MetOpen ` ( normh o. -h ) ) e. ( TopOn ` ~H ) )
24 17 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
25 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
26 17 24 25 19 21 h2hlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) )
27 resss 
 |-  ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) ) C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
28 26 27 eqsstri 
 |-  ~~>v C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
29 28 ssbri 
 |-  ( F ~~>v A -> F ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) A )
30 3 29 syl 
 |-  ( ph -> F ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) A )
31 28 ssbri 
 |-  ( G ~~>v B -> G ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) B )
32 4 31 syl 
 |-  ( ph -> G ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) B )
33 17 hhva 
 |-  +h = ( +v ` <. <. +h , .h >. , normh >. )
34 19 21 33 vacn 
 |-  ( <. <. +h , .h >. , normh >. e. NrmCVec -> +h e. ( ( ( MetOpen ` ( normh o. -h ) ) tX ( MetOpen ` ( normh o. -h ) ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
35 24 34 mp1i 
 |-  ( ph -> +h e. ( ( ( MetOpen ` ( normh o. -h ) ) tX ( MetOpen ` ( normh o. -h ) ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
36 15 16 23 23 1 2 30 32 35 5 lmcn2 
 |-  ( ph -> H ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( A +h B ) )
37 26 breqi 
 |-  ( H ~~>v ( A +h B ) <-> H ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) ) ( A +h B ) )
38 ovex 
 |-  ( A +h B ) e. _V
39 38 brresi 
 |-  ( H ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) ) ( A +h B ) <-> ( H e. ( ~H ^m NN ) /\ H ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( A +h B ) ) )
40 37 39 bitri 
 |-  ( H ~~>v ( A +h B ) <-> ( H e. ( ~H ^m NN ) /\ H ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( A +h B ) ) )
41 14 36 40 sylanbrc 
 |-  ( ph -> H ~~>v ( A +h B ) )