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

Definition df-bra 22430
Description: Define the bra of a vector used by Dirac notation. Based on definition of bra in [Prugovecki] p. 186 (p. 180 in 1971 edition). In Dirac bra-ket notation,  <. A  |  B >. is a complex number equal to the inner product  ( B  .ih  A ). But physicists like to talk about the individual components 
<. A  | and  |  B >., called bra and ket respectively. In order for their properties to make sense formally, we define the ket  |  B >. as the vector  B itself, and the bra  <. A  | as a functional from  ~H to  CC. We represent the Dirac notation  <. A  |  B >. by  ( ( bra `  A
) `  B ); see braval 22524. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 21663) but is also required in order for the associative law kbass2 22697 to work.

Our definition of bra and the associated outer product df-kb 22431 differs from, but is equivalent to, a common approach in the literature that makes use of mappings to a dual space. Our approach eliminates the need to have a parallel development of this dual space and instead keeps everything in Hilbert space.

For an extensive discussion about how our notation maps to the bra-ket notation in physics textbooks, see http://us.metamath.org/mpeuni/mmnotes.txt, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)

Assertion
Ref Expression
df-bra  |-  bra  =  ( x  e.  ~H  |->  ( y  e.  ~H  |->  ( y  .ih  x
) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-bra
StepHypRef Expression
1 cbr 21536 . 2  class  bra
2 vx . . 3  set  x
3 chil 21499 . . 3  class  ~H
4 vy . . . 4  set  y
54cv 1622 . . . . 5  class  y
62cv 1622 . . . . 5  class  x
7 csp 21502 . . . . 5  class  .ih
85, 6, 7co 5858 . . . 4  class  ( y 
.ih  x )
94, 3, 8cmpt 4077 . . 3  class  ( y  e.  ~H  |->  ( y 
.ih  x ) )
102, 3, 9cmpt 4077 . 2  class  ( x  e.  ~H  |->  ( y  e.  ~H  |->  ( y 
.ih  x ) ) )
111, 10wceq 1623 1  wff  bra  =  ( x  e.  ~H  |->  ( y  e.  ~H  |->  ( y  .ih  x
) ) )
Colors of variables: wff set class
This definition is referenced by:  brafval  22523  rnbra  22687  bra11  22688
  Copyright terms: Public domain W3C validator