Metamath Proof Explorer

Theorem hhcno

Description: The continuous operators 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 )
Assertion hhcno 
|- ContOp = ( J Cn J )

Proof

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