HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-cnop Unicode version

Definition df-cnop 22366
Description: Define the set of continuous operators on Hilbert space. For every "epsilon" ( y) there is an "delta" ( z) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-cnop  |-  ConOp  =  {
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 ) }
Distinct variable group:    w, t, x, y, z

Detailed syntax breakdown of Definition df-cnop
StepHypRef Expression
1 ccop 21472 . 2  class  ConOp
2 vw . . . . . . . . . . . 12  set  w
32cv 1618 . . . . . . . . . . 11  class  w
4 vx . . . . . . . . . . . 12  set  x
54cv 1618 . . . . . . . . . . 11  class  x
6 cmv 21451 . . . . . . . . . . 11  class  -h
73, 5, 6co 5778 . . . . . . . . . 10  class  ( w  -h  x )
8 cno 21449 . . . . . . . . . 10  class  normh
97, 8cfv 4659 . . . . . . . . 9  class  ( normh `  ( w  -h  x
) )
10 vz . . . . . . . . . 10  set  z
1110cv 1618 . . . . . . . . 9  class  z
12 clt 8821 . . . . . . . . 9  class  <
139, 11, 12wbr 3983 . . . . . . . 8  wff  ( normh `  ( w  -h  x
) )  <  z
14 vt . . . . . . . . . . . . 13  set  t
1514cv 1618 . . . . . . . . . . . 12  class  t
163, 15cfv 4659 . . . . . . . . . . 11  class  ( t `
 w )
175, 15cfv 4659 . . . . . . . . . . 11  class  ( t `
 x )
1816, 17, 6co 5778 . . . . . . . . . 10  class  ( ( t `  w )  -h  ( t `  x ) )
1918, 8cfv 4659 . . . . . . . . 9  class  ( normh `  ( ( t `  w )  -h  (
t `  x )
) )
20 vy . . . . . . . . . 10  set  y
2120cv 1618 . . . . . . . . 9  class  y
2219, 21, 12wbr 3983 . . . . . . . 8  wff  ( normh `  ( ( t `  w )  -h  (
t `  x )
) )  <  y
2313, 22wi 6 . . . . . . 7  wff  ( (
normh `  ( w  -h  x ) )  < 
z  ->  ( normh `  ( ( t `  w )  -h  (
t `  x )
) )  <  y
)
24 chil 21445 . . . . . . 7  class  ~H
2523, 2, 24wral 2516 . . . . . 6  wff  A. w  e.  ~H  ( ( normh `  ( w  -h  x
) )  <  z  ->  ( normh `  ( (
t `  w )  -h  ( t `  x
) ) )  < 
y )
26 crp 10307 . . . . . 6  class  RR+
2725, 10, 26wrex 2517 . . . . 5  wff  E. z  e.  RR+  A. w  e. 
~H  ( ( normh `  ( w  -h  x
) )  <  z  ->  ( normh `  ( (
t `  w )  -h  ( t `  x
) ) )  < 
y )
2827, 20, 26wral 2516 . . . 4  wff  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  ~H  ( ( normh `  (
w  -h  x ) )  <  z  -> 
( normh `  ( (
t `  w )  -h  ( t `  x
) ) )  < 
y )
2928, 4, 24wral 2516 . . 3  wff  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
)
30 cmap 6726 . . . 4  class  ^m
3124, 24, 30co 5778 . . 3  class  ( ~H 
^m  ~H )
3229, 14, 31crab 2520 . 2  class  { 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 ) }
331, 32wceq 1619 1  wff  ConOp  =  {
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 ) }
Colors of variables: wff set class
This definition is referenced by:  elcnop  22383  hhcno  22430
  Copyright terms: Public domain W3C validator