Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-kb Unicode version

Definition df-kb 22261
 Description: Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, is an operator known as the outer product of and , which we represent by . Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with definition df-bra 22260, 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.)
Assertion
Ref Expression
df-kb
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-kb
StepHypRef Expression
1 ck 21367 . 2
2 vx . . 3
3 vy . . 3
4 chil 21329 . . 3
5 vz . . . 4
65cv 1618 . . . . . 6
73cv 1618 . . . . . 6
8 csp 21332 . . . . . 6
96, 7, 8co 5710 . . . . 5
102cv 1618 . . . . 5
11 csm 21331 . . . . 5
129, 10, 11co 5710 . . . 4
135, 4, 12cmpt 3974 . . 3
142, 3, 4, 4, 13cmpt2 5712 . 2
151, 14wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  kbfval  22362
 Copyright terms: Public domain W3C validator