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

Definition df-kb 29678
 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 29677, 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 28784 . 2 class ketbra
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 chba 28746 . . 3 class
5 vz . . . 4 setvar 𝑧
65cv 1537 . . . . . 6 class 𝑧
73cv 1537 . . . . . 6 class 𝑦
8 csp 28749 . . . . . 6 class ·ih
96, 7, 8co 7145 . . . . 5 class (𝑧 ·ih 𝑦)
102cv 1537 . . . . 5 class 𝑥
11 csm 28748 . . . . 5 class ·
129, 10, 11co 7145 . . . 4 class ((𝑧 ·ih 𝑦) · 𝑥)
135, 4, 12cmpt 5114 . . 3 class (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) · 𝑥))
142, 3, 4, 4, 13cmpo 7147 . 2 class (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) · 𝑥)))
151, 14wceq 1538 1 wff ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) · 𝑥)))
 Colors of variables: wff setvar class This definition is referenced by:  kbfval  29779
 Copyright terms: Public domain W3C validator