Step |
Hyp |
Ref |
Expression |
1 |
|
h2hc.1 |
|- U = <. <. +h , .h >. , normh >. |
2 |
|
h2hc.2 |
|- U e. NrmCVec |
3 |
|
h2hc.3 |
|- ~H = ( BaseSet ` U ) |
4 |
|
h2hc.4 |
|- D = ( IndMet ` U ) |
5 |
|
df-rab |
|- { f e. ( ~H ^m NN ) | A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x } = { f | ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) } |
6 |
|
df-hcau |
|- Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x } |
7 |
|
elin |
|- ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) ) |
8 |
|
ancom |
|- ( ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) <-> ( f e. ( ~H ^m NN ) /\ f e. ( Cau ` D ) ) ) |
9 |
3
|
hlex |
|- ~H e. _V |
10 |
|
nnex |
|- NN e. _V |
11 |
9 10
|
elmap |
|- ( f e. ( ~H ^m NN ) <-> f : NN --> ~H ) |
12 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
13 |
3 4
|
imsxmet |
|- ( U e. NrmCVec -> D e. ( *Met ` ~H ) ) |
14 |
2 13
|
mp1i |
|- ( f : NN --> ~H -> D e. ( *Met ` ~H ) ) |
15 |
|
1zzd |
|- ( f : NN --> ~H -> 1 e. ZZ ) |
16 |
|
eqidd |
|- ( ( f : NN --> ~H /\ k e. NN ) -> ( f ` k ) = ( f ` k ) ) |
17 |
|
eqidd |
|- ( ( f : NN --> ~H /\ j e. NN ) -> ( f ` j ) = ( f ` j ) ) |
18 |
|
id |
|- ( f : NN --> ~H -> f : NN --> ~H ) |
19 |
12 14 15 16 17 18
|
iscauf |
|- ( f : NN --> ~H -> ( f e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x ) ) |
20 |
|
ffvelrn |
|- ( ( f : NN --> ~H /\ j e. NN ) -> ( f ` j ) e. ~H ) |
21 |
20
|
adantr |
|- ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( f ` j ) e. ~H ) |
22 |
|
eluznn |
|- ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN ) |
23 |
|
ffvelrn |
|- ( ( f : NN --> ~H /\ k e. NN ) -> ( f ` k ) e. ~H ) |
24 |
22 23
|
sylan2 |
|- ( ( f : NN --> ~H /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( f ` k ) e. ~H ) |
25 |
24
|
anassrs |
|- ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( f ` k ) e. ~H ) |
26 |
1 2 3 4
|
h2hmetdval |
|- ( ( ( f ` j ) e. ~H /\ ( f ` k ) e. ~H ) -> ( ( f ` j ) D ( f ` k ) ) = ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) ) |
27 |
21 25 26
|
syl2anc |
|- ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( f ` j ) D ( f ` k ) ) = ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) ) |
28 |
27
|
breq1d |
|- ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( f ` j ) D ( f ` k ) ) < x <-> ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
29 |
28
|
ralbidva |
|- ( ( f : NN --> ~H /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x <-> A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
30 |
29
|
rexbidva |
|- ( f : NN --> ~H -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
31 |
30
|
ralbidv |
|- ( f : NN --> ~H -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
32 |
19 31
|
bitrd |
|- ( f : NN --> ~H -> ( f e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
33 |
11 32
|
sylbi |
|- ( f e. ( ~H ^m NN ) -> ( f e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
34 |
33
|
pm5.32i |
|- ( ( f e. ( ~H ^m NN ) /\ f e. ( Cau ` D ) ) <-> ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
35 |
7 8 34
|
3bitri |
|- ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) ) |
36 |
35
|
abbi2i |
|- ( ( Cau ` D ) i^i ( ~H ^m NN ) ) = { f | ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) } |
37 |
5 6 36
|
3eqtr4i |
|- Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) ) |