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

Definition df-adjh 22429
Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of  adjh is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 22663) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-adjh  |-  adjh  =  { <. t ,  u >.  |  ( t : ~H --> ~H  /\  u : ~H --> ~H  /\  A. x  e.  ~H  A. y  e. 
~H  ( ( t `
 x )  .ih  y )  =  ( x  .ih  ( u `
 y ) ) ) }
Distinct variable group:    u, t, x, y

Detailed syntax breakdown of Definition df-adjh
StepHypRef Expression
1 cado 21535 . 2  class  adjh
2 chil 21499 . . . . 5  class  ~H
3 vt . . . . . 6  set  t
43cv 1622 . . . . 5  class  t
52, 2, 4wf 5251 . . . 4  wff  t : ~H --> ~H
6 vu . . . . . 6  set  u
76cv 1622 . . . . 5  class  u
82, 2, 7wf 5251 . . . 4  wff  u : ~H --> ~H
9 vx . . . . . . . . . 10  set  x
109cv 1622 . . . . . . . . 9  class  x
1110, 4cfv 5255 . . . . . . . 8  class  ( t `
 x )
12 vy . . . . . . . . 9  set  y
1312cv 1622 . . . . . . . 8  class  y
14 csp 21502 . . . . . . . 8  class  .ih
1511, 13, 14co 5858 . . . . . . 7  class  ( ( t `  x ) 
.ih  y )
1613, 7cfv 5255 . . . . . . . 8  class  ( u `
 y )
1710, 16, 14co 5858 . . . . . . 7  class  ( x 
.ih  ( u `  y ) )
1815, 17wceq 1623 . . . . . 6  wff  ( ( t `  x ) 
.ih  y )  =  ( x  .ih  (
u `  y )
)
1918, 12, 2wral 2543 . . . . 5  wff  A. y  e.  ~H  ( ( t `
 x )  .ih  y )  =  ( x  .ih  ( u `
 y ) )
2019, 9, 2wral 2543 . . . 4  wff  A. x  e.  ~H  A. y  e. 
~H  ( ( t `
 x )  .ih  y )  =  ( x  .ih  ( u `
 y ) )
215, 8, 20w3a 934 . . 3  wff  ( t : ~H --> ~H  /\  u : ~H --> ~H  /\  A. x  e.  ~H  A. y  e.  ~H  (
( t `  x
)  .ih  y )  =  ( x  .ih  ( u `  y
) ) )
2221, 3, 6copab 4076 . 2  class  { <. t ,  u >.  |  ( t : ~H --> ~H  /\  u : ~H --> ~H  /\  A. x  e.  ~H  A. y  e.  ~H  (
( t `  x
)  .ih  y )  =  ( x  .ih  ( u `  y
) ) ) }
231, 22wceq 1623 1  wff  adjh  =  { <. t ,  u >.  |  ( t : ~H --> ~H  /\  u : ~H --> ~H  /\  A. x  e.  ~H  A. y  e. 
~H  ( ( t `
 x )  .ih  y )  =  ( x  .ih  ( u `
 y ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  dfadj2  22465  adjeq  22515
  Copyright terms: Public domain W3C validator