**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, is a complex number equal to the inner
product . But physicists like to talk about the
individual components
and , called bra and ket
respectively. In order for their properties to make sense formally, we
define the ket
as the vector itself, and the bra
as a functional from to . We represent the
Dirac notation by ; 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.) |