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