Definition df-bra 9776

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 H~ to CC. We represent the Dirac notation <.A | B>. by ((bra` A)` B); see bravalvalt 9868. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 8951) but is also required in order for the associative law kbass2t 10050 to work.

Our definition of bra and the associated outer product df-kb 9777 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 e. H~ /\ t = {<.y, z>. | (y e. H~ /\ z = (y .ih x))})}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-bra

Step	Hyp	Ref	Expression
1		cbr 8825	. 2 class bra
2		vx	. . . . . 6 set x
3	2	cv 955	. . . . 5 class x
4		chil 8788	. . . . 5 class H~
5	3, 4	wcel 958	. . . 4 wff x e. H~
6		vt	. . . . . 6 set t
7	6	cv 955	. . . . 5 class t
8		vy	. . . . . . . . 9 set y
9	8	cv 955	. . . . . . . 8 class y
10	9, 4	wcel 958	. . . . . . 7 wff y e. H~
11		vz	. . . . . . . . 9 set z
12	11	cv 955	. . . . . . . 8 class z
13		csp 8793	. . . . . . . . 9 class .ih
14	9, 3, 13	co 3963	. . . . . . . 8 class (y .ih x)
15	12, 14	wceq 956	. . . . . . 7 wff z = (y .ih x)
16	10, 15	wa 223	. . . . . 6 wff (y e. H~ /\ z = (y .ih x))
17	16, 8, 11	copab 2666	. . . . 5 class {<.y, z>. | (y e. H~ /\ z = (y .ih x))}
18	7, 17	wceq 956	. . . 4 wff t = {<.y, z>. | (y e. H~ /\ z = (y .ih x))}
19	5, 18	wa 223	. . 3 wff (x e. H~ /\ t = {<.y, z>. | (y e. H~ /\ z = (y .ih x))})
20	19, 2, 6	copab 2666	. 2 class {<.x, t>. | (x e. H~ /\ t = {<.y, z>. | (y e. H~ /\ z = (y .ih x))})}
21	1, 20	wceq 956	1 wff bra = {<.x, t>. | (x e. H~ /\ t = {<.y, z>. | (y e. H~ /\ z = (y .ih x))})}

This definition is referenced by:  bravalt 9867  rnbra 10040  bra11 10041

Copyright terms: Public domain