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

Definition df-bra 30220
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 (𝐵 ·ih 𝐴). 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 ((bra‘𝐴)‘𝐵); see braval 30314. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 29454) but is also required in order for the associative law kbass2 30487 to work.

Our definition of bra and the associated outer product df-kb 30221 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 30221, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)

Assertion
Ref Expression
df-bra bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bra
StepHypRef Expression
1 cbr 29326 . 2 class bra
2 vx . . 3 setvar 𝑥
3 chba 29289 . . 3 class
4 vy . . . 4 setvar 𝑦
54cv 1538 . . . . 5 class 𝑦
62cv 1538 . . . . 5 class 𝑥
7 csp 29292 . . . . 5 class ·ih
85, 6, 7co 7267 . . . 4 class (𝑦 ·ih 𝑥)
94, 3, 8cmpt 5156 . . 3 class (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥))
102, 3, 9cmpt 5156 . 2 class (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
111, 10wceq 1539 1 wff bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  brafval  30313  rnbra  30477  bra11  30478
  Copyright terms: Public domain W3C validator