Metamath Proof Explorer


Definition df-bra

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 ( ( braA )B ) ; see braval . The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 ) but is also required in order for the associative law kbass2 to work.

Our definition of bra and the associated outer product df-kb 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 mmnotes.txt , under the 17-May-2006 entry. (Contributed by NM, 15-May-2006) (New usage is discouraged.)

Ref Expression
Assertion df-bra
|- bra = ( x e. ~H |-> ( y e. ~H |-> ( y .ih x ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbr
 |-  bra
1 vx
 |-  x
2 chba
 |-  ~H
3 vy
 |-  y
4 3 cv
 |-  y
5 csp
 |-  .ih
6 1 cv
 |-  x
7 4 6 5 co
 |-  ( y .ih x )
8 3 2 7 cmpt
 |-  ( y e. ~H |-> ( y .ih x ) )
9 1 2 8 cmpt
 |-  ( x e. ~H |-> ( y e. ~H |-> ( y .ih x ) ) )
10 0 9 wceq
 |-  bra = ( x e. ~H |-> ( y e. ~H |-> ( y .ih x ) ) )