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

Definition df-lnop 22251
Description: Define the set of linear operators on Hilbert space. (See df-hosum 21992 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-lnop  |-  LinOp  =  {
t  e.  ( ~H 
^m  ~H )  |  A. x  e.  CC  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  .h  (
t `  y )
)  +h  ( t `
 z ) ) }
Distinct variable group:    x, t, y, z

Detailed syntax breakdown of Definition df-lnop
StepHypRef Expression
1 clo 21357 . 2  class  LinOp
2 vx . . . . . . . . . . 11  set  x
32cv 1618 . . . . . . . . . 10  class  x
4 vy . . . . . . . . . . 11  set  y
54cv 1618 . . . . . . . . . 10  class  y
6 csm 21331 . . . . . . . . . 10  class  .h
73, 5, 6co 5710 . . . . . . . . 9  class  ( x  .h  y )
8 vz . . . . . . . . . 10  set  z
98cv 1618 . . . . . . . . 9  class  z
10 cva 21330 . . . . . . . . 9  class  +h
117, 9, 10co 5710 . . . . . . . 8  class  ( ( x  .h  y )  +h  z )
12 vt . . . . . . . . 9  set  t
1312cv 1618 . . . . . . . 8  class  t
1411, 13cfv 4592 . . . . . . 7  class  ( t `
 ( ( x  .h  y )  +h  z ) )
155, 13cfv 4592 . . . . . . . . 9  class  ( t `
 y )
163, 15, 6co 5710 . . . . . . . 8  class  ( x  .h  ( t `  y ) )
179, 13cfv 4592 . . . . . . . 8  class  ( t `
 z )
1816, 17, 10co 5710 . . . . . . 7  class  ( ( x  .h  ( t `
 y ) )  +h  ( t `  z ) )
1914, 18wceq 1619 . . . . . 6  wff  ( t `
 ( ( x  .h  y )  +h  z ) )  =  ( ( x  .h  ( t `  y
) )  +h  (
t `  z )
)
20 chil 21329 . . . . . 6  class  ~H
2119, 8, 20wral 2509 . . . . 5  wff  A. z  e.  ~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  .h  (
t `  y )
)  +h  ( t `
 z ) )
2221, 4, 20wral 2509 . . . 4  wff  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  .h  (
t `  y )
)  +h  ( t `
 z ) )
23 cc 8615 . . . 4  class  CC
2422, 2, 23wral 2509 . . 3  wff  A. x  e.  CC  A. y  e. 
~H  A. z  e.  ~H  ( t `  (
( x  .h  y
)  +h  z ) )  =  ( ( x  .h  ( t `
 y ) )  +h  ( t `  z ) )
25 cmap 6658 . . . 4  class  ^m
2620, 20, 25co 5710 . . 3  class  ( ~H 
^m  ~H )
2724, 12, 26crab 2512 . 2  class  { t  e.  ( ~H  ^m  ~H )  |  A. x  e.  CC  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  .h  (
t `  y )
)  +h  ( t `
 z ) ) }
281, 27wceq 1619 1  wff  LinOp  =  {
t  e.  ( ~H 
^m  ~H )  |  A. x  e.  CC  A. y  e.  ~H  A. z  e. 
~H  ( t `  ( ( x  .h  y )  +h  z
) )  =  ( ( x  .h  (
t `  y )
)  +h  ( t `
 z ) ) }
Colors of variables: wff set class
This definition is referenced by:  ellnop  22268  hhlnoi  22310
  Copyright terms: Public domain W3C validator