Definition df-kb

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 , 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
Assertion	df-kb	⊢ ketbra = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑧 ∈ ℋ ↦ ( ( 𝑧 ·ih 𝑦 ) ·ℎ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ck	⊢ ketbra
1		vx	⊢ 𝑥
2		chba	⊢ ℋ
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5	4	cv	⊢ 𝑧
6		csp	⊢ ·ih
7	3	cv	⊢ 𝑦
8	5 7 6	co	⊢ ( 𝑧 ·ih 𝑦 )
9		csm	⊢ ·ℎ
10	1	cv	⊢ 𝑥
11	8 10 9	co	⊢ ( ( 𝑧 ·ih 𝑦 ) ·ℎ 𝑥 )
12	4 2 11	cmpt	⊢ ( 𝑧 ∈ ℋ ↦ ( ( 𝑧 ·ih 𝑦 ) ·ℎ 𝑥 ) )
13	1 3 2 2 12	cmpo	⊢ ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑧 ∈ ℋ ↦ ( ( 𝑧 ·ih 𝑦 ) ·ℎ 𝑥 ) ) )
14	0 13	wceq	⊢ ketbra = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑧 ∈ ℋ ↦ ( ( 𝑧 ·ih 𝑦 ) ·ℎ 𝑥 ) ) )