Definition df-kb 29282

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 29281, 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

Step	Hyp	Ref	Expression
1		ck 28386	. 2 class ketbra
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		chba 28348	. . 3 class ℋ
5		vz	. . . 4 setvar 𝑧
6	5	cv 1600	. . . . . 6 class 𝑧
7	3	cv 1600	. . . . . 6 class 𝑦
8		csp 28351	. . . . . 6 class ·ih
9	6, 7, 8	co 6922	. . . . 5 class (𝑧 ·ih 𝑦)
10	2	cv 1600	. . . . 5 class 𝑥
11		csm 28350	. . . . 5 class ·ℎ
12	9, 10, 11	co 6922	. . . 4 class ((𝑧 ·ih 𝑦) ·ℎ 𝑥)
13	5, 4, 12	cmpt 4965	. . 3 class (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥))
14	2, 3, 4, 4, 13	cmpt2 6924	. 2 class (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥)))
15	1, 14	wceq 1601	1 wff ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥)))

This definition is referenced by:  kbfval  29383