![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > df-kb | Structured version Visualization version GIF 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 (๐ด ketbra ๐ต). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with Definition df-bra 31103, 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 | โข ketbra = (๐ฅ โ โ, ๐ฆ โ โ โฆ (๐ง โ โ โฆ ((๐ง ยทih ๐ฆ) ยทโ ๐ฅ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ck 30210 | . 2 class ketbra | |
2 | vx | . . 3 setvar ๐ฅ | |
3 | vy | . . 3 setvar ๐ฆ | |
4 | chba 30172 | . . 3 class โ | |
5 | vz | . . . 4 setvar ๐ง | |
6 | 5 | cv 1541 | . . . . . 6 class ๐ง |
7 | 3 | cv 1541 | . . . . . 6 class ๐ฆ |
8 | csp 30175 | . . . . . 6 class ยทih | |
9 | 6, 7, 8 | co 7409 | . . . . 5 class (๐ง ยทih ๐ฆ) |
10 | 2 | cv 1541 | . . . . 5 class ๐ฅ |
11 | csm 30174 | . . . . 5 class ยทโ | |
12 | 9, 10, 11 | co 7409 | . . . 4 class ((๐ง ยทih ๐ฆ) ยทโ ๐ฅ) |
13 | 5, 4, 12 | cmpt 5232 | . . 3 class (๐ง โ โ โฆ ((๐ง ยทih ๐ฆ) ยทโ ๐ฅ)) |
14 | 2, 3, 4, 4, 13 | cmpo 7411 | . 2 class (๐ฅ โ โ, ๐ฆ โ โ โฆ (๐ง โ โ โฆ ((๐ง ยทih ๐ฆ) ยทโ ๐ฅ))) |
15 | 1, 14 | wceq 1542 | 1 wff ketbra = (๐ฅ โ โ, ๐ฆ โ โ โฆ (๐ง โ โ โฆ ((๐ง ยทih ๐ฆ) ยทโ ๐ฅ))) |
Colors of variables: wff setvar class |
This definition is referenced by: kbfval 31205 |
Copyright terms: Public domain | W3C validator |