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 = ( 𝑥 ∈ ℋ ↦ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cbr | ⊢ bra | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | chba | ⊢ ℋ | |
| 3 | vy | ⊢ 𝑦 | |
| 4 | 3 | cv | ⊢ 𝑦 |
| 5 | csp | ⊢ ·ih | |
| 6 | 1 | cv | ⊢ 𝑥 |
| 7 | 4 6 5 | co | ⊢ ( 𝑦 ·ih 𝑥 ) |
| 8 | 3 2 7 | cmpt | ⊢ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) |
| 9 | 1 2 8 | cmpt | ⊢ ( 𝑥 ∈ ℋ ↦ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) ) |
| 10 | 0 9 | wceq | ⊢ bra = ( 𝑥 ∈ ℋ ↦ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) ) |