# 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 ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)\mathrm{bra}\left({C}\right)\left({D}\right)=\left(\mathrm{bra}\left({A}\right)\left({B}\right){·}_{\mathrm{fn}}\mathrm{bra}\left({C}\right)\right)\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 bracl ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)\in ℂ$
2 1 adantr ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)\in ℂ$
3 brafn ${⊢}{C}\in ℋ\to \mathrm{bra}\left({C}\right):ℋ⟶ℂ$
4 3 ad2antrl ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \mathrm{bra}\left({C}\right):ℋ⟶ℂ$
5 simprr ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {D}\in ℋ$
6 hfmval ${⊢}\left(\mathrm{bra}\left({A}\right)\left({B}\right)\in ℂ\wedge \mathrm{bra}\left({C}\right):ℋ⟶ℂ\wedge {D}\in ℋ\right)\to \left(\mathrm{bra}\left({A}\right)\left({B}\right){·}_{\mathrm{fn}}\mathrm{bra}\left({C}\right)\right)\left({D}\right)=\mathrm{bra}\left({A}\right)\left({B}\right)\mathrm{bra}\left({C}\right)\left({D}\right)$
7 2 4 5 6 syl3anc ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left(\mathrm{bra}\left({A}\right)\left({B}\right){·}_{\mathrm{fn}}\mathrm{bra}\left({C}\right)\right)\left({D}\right)=\mathrm{bra}\left({A}\right)\left({B}\right)\mathrm{bra}\left({C}\right)\left({D}\right)$
8 7 eqcomd ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)\mathrm{bra}\left({C}\right)\left({D}\right)=\left(\mathrm{bra}\left({A}\right)\left({B}\right){·}_{\mathrm{fn}}\mathrm{bra}\left({C}\right)\right)\left({D}\right)$