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

Definition df-bra 28837
 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 28931. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 28069) but is also required in order for the associative law kbass2 29104 to work. Our definition of bra and the associated outer product df-kb 28838 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.)
Assertion
Ref Expression
df-bra bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bra
StepHypRef Expression
1 cbr 27941 . 2 class bra
2 vx . . 3 setvar 𝑥
3 chil 27904 . . 3 class
4 vy . . . 4 setvar 𝑦
54cv 1522 . . . . 5 class 𝑦
62cv 1522 . . . . 5 class 𝑥
7 csp 27907 . . . . 5 class ·ih
85, 6, 7co 6690 . . . 4 class (𝑦 ·ih 𝑥)
94, 3, 8cmpt 4762 . . 3 class (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥))
102, 3, 9cmpt 4762 . 2 class (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
111, 10wceq 1523 1 wff bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
 Colors of variables: wff setvar class This definition is referenced by:  brafval  28930  rnbra  29094  bra11  29095
 Copyright terms: Public domain W3C validator