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 ) )