Metamath Proof Explorer

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 = x ∈ ℋ , y ∈ ℋ ⟼ z ∈ ℋ ⟼ z ⋅ ih y ⋅ ℎ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ck class ketbra
1 vx setvar x
2 chba class ℋ
3 vy setvar y
4 vz setvar z
5 4 cv setvar z
6 csp class ⋅ ih
7 3 cv setvar y
8 5 7 6 co class z ⋅ ih y
9 csm class ⋅ ℎ
10 1 cv setvar x
11 8 10 9 co class z ⋅ ih y ⋅ ℎ x
12 4 2 11 cmpt class z ∈ ℋ ⟼ z ⋅ ih y ⋅ ℎ x
13 1 3 2 2 12 cmpo class x ∈ ℋ , y ∈ ℋ ⟼ z ∈ ℋ ⟼ z ⋅ ih y ⋅ ℎ x
14 0 13 wceq wff ketbra = x ∈ ℋ , y ∈ ℋ ⟼ z ∈ ℋ ⟼ z ⋅ ih y ⋅ ℎ x