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

Definition df-kb 23355
Description: Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation,  |  A >.  <. B  | is an operator known as the outer product of  A and  B, which we represent by  ( A  ketbra  B ). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with definition df-bra 23354, allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-kb  |-  ketbra  =  ( x  e.  ~H , 
y  e.  ~H  |->  ( z  e.  ~H  |->  ( ( z  .ih  y
)  .h  x ) ) )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-kb
StepHypRef Expression
1 ck 22461 . 2  class  ketbra
2 vx . . 3  set  x
3 vy . . 3  set  y
4 chil 22423 . . 3  class  ~H
5 vz . . . 4  set  z
65cv 1652 . . . . . 6  class  z
73cv 1652 . . . . . 6  class  y
8 csp 22426 . . . . . 6  class  .ih
96, 7, 8co 6082 . . . . 5  class  ( z 
.ih  y )
102cv 1652 . . . . 5  class  x
11 csm 22425 . . . . 5  class  .h
129, 10, 11co 6082 . . . 4  class  ( ( z  .ih  y )  .h  x )
135, 4, 12cmpt 4267 . . 3  class  ( z  e.  ~H  |->  ( ( z  .ih  y )  .h  x ) )
142, 3, 4, 4, 13cmpt2 6084 . 2  class  ( x  e.  ~H ,  y  e.  ~H  |->  ( z  e.  ~H  |->  ( ( z  .ih  y )  .h  x ) ) )
151, 14wceq 1653 1  wff  ketbra  =  ( x  e.  ~H , 
y  e.  ~H  |->  ( z  e.  ~H  |->  ( ( z  .ih  y
)  .h  x ) ) )
Colors of variables: wff set class
This definition is referenced by:  kbfval  23456
  Copyright terms: Public domain W3C validator