Definition df-bra 9693

Description: Define the bra of a vector used by Dirac notation. Based on definition of bra in [Prugovecki] p. 186. 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 ℋ to ℂ. We represent the Dirac notation ⟨A∣B⟩ by ((bra ‘A) ‘B); see bravalvalt 9784. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 8872) but is also required in order for the associative law kbass2t 9962 to work.

Our definition of bra and the associated outer product df-kb 9694 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/mpegif/mmnotes.txt, under the 17-May-2006 entry.

Assertion

Ref	Expression
df-bra	⊢ bra = {⟨x, t⟩∣(x ∈ ℋ ⋀ t = {⟨y, z⟩∣(y ∈ ℋ ⋀ z = (y ·ih x))})}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-bra

Step	Hyp	Ref	Expression
1		cbr 8764	. 2 class bra
2		vx	. . . . . 6 set x
3	2	cv 952	. . . . 5 class x
4		chil 8727	. . . . 5 class ℋ
5	3, 4	wcel 955	. . . 4 wff x ∈ ℋ
6		vt	. . . . . 6 set t
7	6	cv 952	. . . . 5 class t
8		vy	. . . . . . . . 9 set y
9	8	cv 952	. . . . . . . 8 class y
10	9, 4	wcel 955	. . . . . . 7 wff y ∈ ℋ
11		vz	. . . . . . . . 9 set z
12	11	cv 952	. . . . . . . 8 class z
13		csp 8732	. . . . . . . . 9 class ·ih
14	9, 3, 13	co 3948	. . . . . . . 8 class (y ·ih x)
15	12, 14	wceq 953	. . . . . . 7 wff z = (y ·ih x)
16	10, 15	wa 223	. . . . . 6 wff (y ∈ ℋ ⋀ z = (y ·ih x))
17	16, 8, 11	copab 2656	. . . . 5 class {⟨y, z⟩∣(y ∈ ℋ ⋀ z = (y ·ih x))}
18	7, 17	wceq 953	. . . 4 wff t = {⟨y, z⟩∣(y ∈ ℋ ⋀ z = (y ·ih x))}
19	5, 18	wa 223	. . 3 wff (x ∈ ℋ ⋀ t = {⟨y, z⟩∣(y ∈ ℋ ⋀ z = (y ·ih x))})
20	19, 2, 6	copab 2656	. 2 class {⟨x, t⟩∣(x ∈ ℋ ⋀ t = {⟨y, z⟩∣(y ∈ ℋ ⋀ z = (y ·ih x))})}
21	1, 20	wceq 953	1 wff bra = {⟨x, t⟩∣(x ∈ ℋ ⋀ t = {⟨y, z⟩∣(y ∈ ℋ ⋀ z = (y ·ih x))})}

This definition is referenced by:  bravalt 9783  rnbra 9953  bra11 9954

Copyright terms: Public domain