Metamath Proof Explorer

Theorem kbass1

Description: Dirac bra-ket associative law ( | A >. <. B | ) | C >. = | A >. ( <. B | C >. ) , i.e., the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since <. B | C >. is a complex number, it is the first argument in the inner product .h that it is mapped to, although in Dirac notation it is placed after the ket. (Contributed by NM, 15-May-2006) (New usage is discouraged.)

Ref Expression
Assertion kbass1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ketbra B ⁡ C = bra ⁡ B ⁡ C ⋅ ℎ A

Proof

Step Hyp Ref Expression
1 kbval ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ketbra B ⁡ C = C ⋅ ih B ⋅ ℎ A
2 braval ⊢ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ B ⁡ C = C ⋅ ih B
3 2 3adant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ B ⁡ C = C ⋅ ih B
4 3 oveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ B ⁡ C ⋅ ℎ A = C ⋅ ih B ⋅ ℎ A
5 1 4 eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ketbra B ⁡ C = bra ⁡ B ⁡ C ⋅ ℎ A