Metamath Proof Explorer

Definition df-bra

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 = (x \in ℋ ⟼ (y \in ℋ ⟼ y \cdot_{ih} x))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbr	$class bra$
1		vx	$setvar x$
2		chba	$class ℋ$
3		vy	$setvar y$
4	3	cv	$setvar y$
5		csp	$class \cdot_{ih}$
6	1	cv	$setvar x$
7	4 6 5	co	$class (y \cdot_{ih} x)$
8	3 2 7	cmpt	$class (y \in ℋ ⟼ y \cdot_{ih} x)$
9	1 2 8	cmpt	$class (x \in ℋ ⟼ (y \in ℋ ⟼ y \cdot_{ih} x))$
10	0 9	wceq	$wff bra = (x \in ℋ ⟼ (y \in ℋ ⟼ y \cdot_{ih} x))$