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

Definition df-kb 31648
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 31647, 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 ketbra = (๐‘ฅ โˆˆ โ„‹, ๐‘ฆ โˆˆ โ„‹ โ†ฆ (๐‘ง โˆˆ โ„‹ โ†ฆ ((๐‘ง ยทih ๐‘ฆ) ยทโ„Ž ๐‘ฅ)))
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐‘ง

Detailed syntax breakdown of Definition df-kb
StepHypRef Expression
1 ck 30754 . 2 class ketbra
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 chba 30716 . . 3 class โ„‹
5 vz . . . 4 setvar ๐‘ง
65cv 1533 . . . . . 6 class ๐‘ง
73cv 1533 . . . . . 6 class ๐‘ฆ
8 csp 30719 . . . . . 6 class ยทih
96, 7, 8co 7414 . . . . 5 class (๐‘ง ยทih ๐‘ฆ)
102cv 1533 . . . . 5 class ๐‘ฅ
11 csm 30718 . . . . 5 class ยทโ„Ž
129, 10, 11co 7414 . . . 4 class ((๐‘ง ยทih ๐‘ฆ) ยทโ„Ž ๐‘ฅ)
135, 4, 12cmpt 5225 . . 3 class (๐‘ง โˆˆ โ„‹ โ†ฆ ((๐‘ง ยทih ๐‘ฆ) ยทโ„Ž ๐‘ฅ))
142, 3, 4, 4, 13cmpo 7416 . 2 class (๐‘ฅ โˆˆ โ„‹, ๐‘ฆ โˆˆ โ„‹ โ†ฆ (๐‘ง โˆˆ โ„‹ โ†ฆ ((๐‘ง ยทih ๐‘ฆ) ยทโ„Ž ๐‘ฅ)))
151, 14wceq 1534 1 wff ketbra = (๐‘ฅ โˆˆ โ„‹, ๐‘ฆ โˆˆ โ„‹ โ†ฆ (๐‘ง โˆˆ โ„‹ โ†ฆ ((๐‘ง ยทih ๐‘ฆ) ยทโ„Ž ๐‘ฅ)))
Colors of variables: wff setvar class
This definition is referenced by:  kbfval  31749
  Copyright terms: Public domain W3C validator