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 y y ih x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbr class bra
1 vx setvar x
2 chba class
3 vy setvar y
4 3 cv setvar y
5 csp class ih
6 1 cv setvar x
7 4 6 5 co class y ih x
8 3 2 7 cmpt class y y ih x
9 1 2 8 cmpt class x y y ih x
10 0 9 wceq wff bra = x y y ih x