Definition df-kb 9717

Description: Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, ∣A⟩ ⟨B∣ is an operator known as the outer product of A and B, which we represent by (A ketbra B). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with definition df-bra 9716, 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.

Assertion

Ref	Expression
df-kb	⊢ ketbra = {⟨⟨x, y⟩, t⟩∣((x ∈ ℋ ⋀ y ∈ ℋ ) ⋀ t = {⟨w, v⟩∣(w ∈ ℋ ⋀ v = ((w ·ih y) ·h x))})}

Distinct variable group:   v,t,w,x,y

Detailed syntax breakdown of Definition df-kb

Step	Hyp	Ref	Expression
1		ck 8765	. 2 class ketbra
2		vx	. . . . . . 7 set x
3	2	cv 953	. . . . . 6 class x
4		chil 8727	. . . . . 6 class ℋ
5	3, 4	wcel 956	. . . . 5 wff x ∈ ℋ
6		vy	. . . . . . 7 set y
7	6	cv 953	. . . . . 6 class y
8	7, 4	wcel 956	. . . . 5 wff y ∈ ℋ
9	5, 8	wa 223	. . . 4 wff (x ∈ ℋ ⋀ y ∈ ℋ )
10		vt	. . . . . 6 set t
11	10	cv 953	. . . . 5 class t
12		vw	. . . . . . . . 9 set w
13	12	cv 953	. . . . . . . 8 class w
14	13, 4	wcel 956	. . . . . . 7 wff w ∈ ℋ
15		vv	. . . . . . . . 9 set v
16	15	cv 953	. . . . . . . 8 class v
17		csp 8732	. . . . . . . . . 10 class ·ih
18	13, 7, 17	co 3954	. . . . . . . . 9 class (w ·ih y)
19		csm 8729	. . . . . . . . 9 class ·h
20	18, 3, 19	co 3954	. . . . . . . 8 class ((w ·ih y) ·h x)
21	16, 20	wceq 954	. . . . . . 7 wff v = ((w ·ih y) ·h x)
22	14, 21	wa 223	. . . . . 6 wff (w ∈ ℋ ⋀ v = ((w ·ih y) ·h x))
23	22, 12, 15	copab 2661	. . . . 5 class {⟨w, v⟩∣(w ∈ ℋ ⋀ v = ((w ·ih y) ·h x))}
24	11, 23	wceq 954	. . . 4 wff t = {⟨w, v⟩∣(w ∈ ℋ ⋀ v = ((w ·ih y) ·h x))}
25	9, 24	wa 223	. . 3 wff ((x ∈ ℋ ⋀ y ∈ ℋ ) ⋀ t = {⟨w, v⟩∣(w ∈ ℋ ⋀ v = ((w ·ih y) ·h x))})
26	25, 2, 6, 10	copab2 3955	. 2 class {⟨⟨x, y⟩, t⟩∣((x ∈ ℋ ⋀ y ∈ ℋ ) ⋀ t = {⟨w, v⟩∣(w ∈ ℋ ⋀ v = ((w ·ih y) ·h x))})}
27	1, 26	wceq 954	1 wff ketbra = {⟨⟨x, y⟩, t⟩∣((x ∈ ℋ ⋀ y ∈ ℋ ) ⋀ t = {⟨w, v⟩∣(w ∈ ℋ ⋀ v = ((w ·ih y) ·h x))})}

This definition is referenced by:  kbvalt 9815

Copyright terms: Public domain