Metamath Proof Explorer

Theorem kbass3

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 kbass3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D = bra ⁡ A ⁡ B · fn bra ⁡ C ⁡ D

Proof

Step Hyp Ref Expression
1 bracl ⊢ A ∈ ℋ ∧ B ∈ ℋ → bra ⁡ A ⁡ B ∈ ℂ
2 1 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ B ∈ ℂ
3 brafn ⊢ C ∈ ℋ → bra ⁡ C : ℋ ⟶ ℂ
4 3 ad2antrl ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ C : ℋ ⟶ ℂ
5 simprr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → D ∈ ℋ
6 hfmval ⊢ bra ⁡ A ⁡ B ∈ ℂ ∧ bra ⁡ C : ℋ ⟶ ℂ ∧ D ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C ⁡ D = bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D
7 2 4 5 6 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C ⁡ D = bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D
8 7 eqcomd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ D = bra ⁡ A ⁡ B · fn bra ⁡ C ⁡ D