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