Metamath Proof Explorer

Theorem hhcnf

Description: The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hhcn.1 
|- D = ( normh o. -h )
hhcn.2 
|- J = ( MetOpen ` D )
hhcn.4 
|- K = ( TopOpen ` CCfld )
Assertion hhcnf 
|- ContFn = ( J Cn K )

Proof

Step Hyp Ref Expression
1 hhcn.1 
 |-  D = ( normh o. -h )
2 hhcn.2 
 |-  J = ( MetOpen ` D )
3 hhcn.4 
 |-  K = ( TopOpen ` CCfld )
4 df-rab 
 |-  { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) } = { t | ( t e. ( CC ^m ~H ) /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) }
5 df-cnfn 
 |-  ContFn = { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }
6 1 hilmetdval 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( x D w ) = ( normh ` ( x -h w ) ) )
7 normsub 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( normh ` ( x -h w ) ) = ( normh ` ( w -h x ) ) )
8 6 7 eqtrd 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( x D w ) = ( normh ` ( w -h x ) ) )
9 8 adantll 
 |-  ( ( ( t : ~H --> CC /\ x e. ~H ) /\ w e. ~H ) -> ( x D w ) = ( normh ` ( w -h x ) ) )
10 9 breq1d 
 |-  ( ( ( t : ~H --> CC /\ x e. ~H ) /\ w e. ~H ) -> ( ( x D w ) < z <-> ( normh ` ( w -h x ) ) < z ) )
11 ffvelrn 
 |-  ( ( t : ~H --> CC /\ x e. ~H ) -> ( t ` x ) e. CC )
12 ffvelrn 
 |-  ( ( t : ~H --> CC /\ w e. ~H ) -> ( t ` w ) e. CC )
13 11 12 anim12dan 
 |-  ( ( t : ~H --> CC /\ ( x e. ~H /\ w e. ~H ) ) -> ( ( t ` x ) e. CC /\ ( t ` w ) e. CC ) )
14 eqid 
 |-  ( abs o. - ) = ( abs o. - )
15 14 cnmetdval 
 |-  ( ( ( t ` x ) e. CC /\ ( t ` w ) e. CC ) -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) = ( abs ` ( ( t ` x ) - ( t ` w ) ) ) )
16 abssub 
 |-  ( ( ( t ` x ) e. CC /\ ( t ` w ) e. CC ) -> ( abs ` ( ( t ` x ) - ( t ` w ) ) ) = ( abs ` ( ( t ` w ) - ( t ` x ) ) ) )
17 15 16 eqtrd 
 |-  ( ( ( t ` x ) e. CC /\ ( t ` w ) e. CC ) -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) = ( abs ` ( ( t ` w ) - ( t ` x ) ) ) )
18 13 17 syl 
 |-  ( ( t : ~H --> CC /\ ( x e. ~H /\ w e. ~H ) ) -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) = ( abs ` ( ( t ` w ) - ( t ` x ) ) ) )
19 18 anassrs 
 |-  ( ( ( t : ~H --> CC /\ x e. ~H ) /\ w e. ~H ) -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) = ( abs ` ( ( t ` w ) - ( t ` x ) ) ) )
20 19 breq1d 
 |-  ( ( ( t : ~H --> CC /\ x e. ~H ) /\ w e. ~H ) -> ( ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y <-> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) )
21 10 20 imbi12d 
 |-  ( ( ( t : ~H --> CC /\ x e. ~H ) /\ w e. ~H ) -> ( ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) <-> ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
22 21 ralbidva 
 |-  ( ( t : ~H --> CC /\ x e. ~H ) -> ( A. w e. ~H ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) <-> A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
23 22 rexbidv 
 |-  ( ( t : ~H --> CC /\ x e. ~H ) -> ( E. z e. RR+ A. w e. ~H ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) <-> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
24 23 ralbidv 
 |-  ( ( t : ~H --> CC /\ x e. ~H ) -> ( A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) <-> A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
25 24 ralbidva 
 |-  ( t : ~H --> CC -> ( A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) <-> A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
26 25 pm5.32i 
 |-  ( ( t : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) ) <-> ( t : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
27 1 hilxmet 
 |-  D e. ( *Met ` ~H )
28 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
29 3 cnfldtopn 
 |-  K = ( MetOpen ` ( abs o. - ) )
30 2 29 metcn 
 |-  ( ( D e. ( *Met ` ~H ) /\ ( abs o. - ) e. ( *Met ` CC ) ) -> ( t e. ( J Cn K ) <-> ( t : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) ) ) )
31 27 28 30 mp2an 
 |-  ( t e. ( J Cn K ) <-> ( t : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( x D w ) < z -> ( ( t ` x ) ( abs o. - ) ( t ` w ) ) < y ) ) )
32 cnex 
 |-  CC e. _V
33 ax-hilex 
 |-  ~H e. _V
34 32 33 elmap 
 |-  ( t e. ( CC ^m ~H ) <-> t : ~H --> CC )
35 34 anbi1i 
 |-  ( ( t e. ( CC ^m ~H ) /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) <-> ( t : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
36 26 31 35 3bitr4i 
 |-  ( t e. ( J Cn K ) <-> ( t e. ( CC ^m ~H ) /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) )
37 36 abbi2i 
 |-  ( J Cn K ) = { t | ( t e. ( CC ^m ~H ) /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) ) }
38 4 5 37 3eqtr4i 
 |-  ContFn = ( J Cn K )