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

Definition df-bra 23306
 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 23400. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 22539) but is also required in order for the associative law kbass2 23573 to work. Our definition of bra and the associated outer product df-kb 23307 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-bra
StepHypRef Expression
1 cbr 22412 . 2
2 vx . . 3
3 chil 22375 . . 3
4 vy . . . 4
54cv 1648 . . . . 5
62cv 1648 . . . . 5
7 csp 22378 . . . . 5
85, 6, 7co 6040 . . . 4
94, 3, 8cmpt 4226 . . 3
102, 3, 9cmpt 4226 . 2
111, 10wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  brafval  23399  rnbra  23563  bra11  23564
 Copyright terms: Public domain W3C validator