|   | 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 31869, 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 30976 | . 2 class ketbra | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | vy | . . 3 setvar 𝑦 | |
| 4 | chba 30938 | . . 3 class ℋ | |
| 5 | vz | . . . 4 setvar 𝑧 | |
| 6 | 5 | cv 1539 | . . . . . 6 class 𝑧 | 
| 7 | 3 | cv 1539 | . . . . . 6 class 𝑦 | 
| 8 | csp 30941 | . . . . . 6 class ·ih | |
| 9 | 6, 7, 8 | co 7431 | . . . . 5 class (𝑧 ·ih 𝑦) | 
| 10 | 2 | cv 1539 | . . . . 5 class 𝑥 | 
| 11 | csm 30940 | . . . . 5 class ·ℎ | |
| 12 | 9, 10, 11 | co 7431 | . . . 4 class ((𝑧 ·ih 𝑦) ·ℎ 𝑥) | 
| 13 | 5, 4, 12 | cmpt 5225 | . . 3 class (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥)) | 
| 14 | 2, 3, 4, 4, 13 | cmpo 7433 | . 2 class (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥))) | 
| 15 | 1, 14 | wceq 1540 | 1 wff ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥))) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: kbfval 31971 | 
| Copyright terms: Public domain | W3C validator |