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 28694
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 28693, 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 27798 . 2 class ketbra
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 chil 27760 . . 3 class
5 vz . . . 4 setvar 𝑧
65cv 1481 . . . . . 6 class 𝑧
73cv 1481 . . . . . 6 class 𝑦
8 csp 27763 . . . . . 6 class ·ih
96, 7, 8co 6647 . . . . 5 class (𝑧 ·ih 𝑦)
102cv 1481 . . . . 5 class 𝑥
11 csm 27762 . . . . 5 class ·
129, 10, 11co 6647 . . . 4 class ((𝑧 ·ih 𝑦) · 𝑥)
135, 4, 12cmpt 4727 . . 3 class (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) · 𝑥))
142, 3, 4, 4, 13cmpt2 6649 . 2 class (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) · 𝑥)))
151, 14wceq 1482 1 wff ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) · 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  kbfval  28795
  Copyright terms: Public domain W3C validator