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 ) ) ) |
| 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 ) ) ) |