Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-kb | Structured version Visualization version Unicode version |
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 28709, 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 |
---|---|
df-kb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ck 27814 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | chil 27776 | . . 3 | |
5 | vz | . . . 4 | |
6 | 5 | cv 1482 | . . . . . 6 |
7 | 3 | cv 1482 | . . . . . 6 |
8 | csp 27779 | . . . . . 6 | |
9 | 6, 7, 8 | co 6650 | . . . . 5 |
10 | 2 | cv 1482 | . . . . 5 |
11 | csm 27778 | . . . . 5 | |
12 | 9, 10, 11 | co 6650 | . . . 4 |
13 | 5, 4, 12 | cmpt 4729 | . . 3 |
14 | 2, 3, 4, 4, 13 | cmpt2 6652 | . 2 |
15 | 1, 14 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: kbfval 28811 |
Copyright terms: Public domain | W3C validator |