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,yzzihyx

Detailed syntax breakdown

Step Hyp Ref Expression
0 ck classketbra
1 vx setvarx
2 chba class
3 vy setvary
4 vz setvarz
5 4 cv setvarz
6 csp classih
7 3 cv setvary
8 5 7 6 co classzihy
9 csm class
10 1 cv setvarx
11 8 10 9 co classzihyx
12 4 2 11 cmpt classzzihyx
13 1 3 2 2 12 cmpo classx,yzzihyx
14 0 13 wceq wffketbra=x,yzzihyx