Metamath Proof Explorer


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 ) ) )