Definition df-kb

Description: Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, | A >. <. B | is an operator known as the outer product of A and B , which we represent by ( A ketbra B ) . Based on Equation 8.1 of Prugovecki p. 376. This definition, combined with Definition df-bra , allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-kb	|- ketbra = ( x e. ~H , y e. ~H |-> ( z e. ~H |-> ( ( z .ih y ) .h x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ck	|- ketbra
1		vx	|- x
2		chba	|- ~H
3		vy	|- y
4		vz	|- z
5	4	cv	|- z
6		csp	|- .ih
7	3	cv	|- y
8	5 7 6	co	|- ( z .ih y )
9		csm	|- .h
10	1	cv	|- x
11	8 10 9	co	|- ( ( z .ih y ) .h x )
12	4 2 11	cmpt	|- ( z e. ~H |-> ( ( z .ih y ) .h x ) )
13	1 3 2 2 12	cmpo	|- ( x e. ~H , y e. ~H |-> ( z e. ~H |-> ( ( z .ih y ) .h x ) ) )
14	0 13	wceq	|- ketbra = ( x e. ~H , y e. ~H |-> ( z e. ~H |-> ( ( z .ih y ) .h x ) ) )