Metamath Proof Explorer

Theorem kbass4

Description: Dirac bra-ket associative law <. A | B >. <. C | D >. = <. A | ( | B >. <. C | D >. ) . (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion kbass4 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D = bra ⁡ A ⁡ bra ⁡ C ⁡ D ⋅ ℎ B

Proof

Step Hyp Ref Expression
1 bracl ⊢ A ∈ ℋ ∧ B ∈ ℋ → bra ⁡ A ⁡ B ∈ ℂ
2 bracl ⊢ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ C ⁡ D ∈ ℂ
3 mulcom ⊢ bra ⁡ A ⁡ B ∈ ℂ ∧ bra ⁡ C ⁡ D ∈ ℂ → bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D = bra ⁡ C ⁡ D ⁢ bra ⁡ A ⁡ B
4 1 2 3 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D = bra ⁡ C ⁡ D ⁢ bra ⁡ A ⁡ B
5 bralnfn ⊢ A ∈ ℋ → bra ⁡ A ∈ LinFn
6 5 ad2antrr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ∈ LinFn
7 2 adantl ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ C ⁡ D ∈ ℂ
8 simplr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → B ∈ ℋ
9 lnfnmul ⊢ bra ⁡ A ∈ LinFn ∧ bra ⁡ C ⁡ D ∈ ℂ ∧ B ∈ ℋ → bra ⁡ A ⁡ bra ⁡ C ⁡ D ⋅ ℎ B = bra ⁡ C ⁡ D ⁢ bra ⁡ A ⁡ B
10 6 7 8 9 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ bra ⁡ C ⁡ D ⋅ ℎ B = bra ⁡ C ⁡ D ⁢ bra ⁡ A ⁡ B
11 4 10 eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D = bra ⁡ A ⁡ bra ⁡ C ⁡ D ⋅ ℎ B