This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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