Metamath Proof Explorer

Theorem kbass6

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 kbass6 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→AketbraB∘CketbraD=Aketbrabra-1⁡bra⁡B∘CketbraD

Proof

Step Hyp Ref Expression
1 kbass5 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→AketbraB∘CketbraD=AketbraB⁡CketbraD
2 kbval ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→AketbraB⁡C=C⋅ihB⋅ℎA
3 2 3expa ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→AketbraB⁡C=C⋅ihB⋅ℎA
4 3 adantrr ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→AketbraB⁡C=C⋅ihB⋅ℎA
5 4 oveq1d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→AketbraB⁡CketbraD=C⋅ihB⋅ℎAketbraD
6 hicl ⊢C∈ℋ∧B∈ℋ→C⋅ihB∈ℂ
7 kbmul ⊢C⋅ihB∈ℂ∧A∈ℋ∧D∈ℋ→C⋅ihB⋅ℎAketbraD=AketbraC⋅ihB‾⋅ℎD
8 6 7 syl3an1 ⊢C∈ℋ∧B∈ℋ∧A∈ℋ∧D∈ℋ→C⋅ihB⋅ℎAketbraD=AketbraC⋅ihB‾⋅ℎD
9 8 3exp ⊢C∈ℋ∧B∈ℋ→A∈ℋ→D∈ℋ→C⋅ihB⋅ℎAketbraD=AketbraC⋅ihB‾⋅ℎD
10 9 ex ⊢C∈ℋ→B∈ℋ→A∈ℋ→D∈ℋ→C⋅ihB⋅ℎAketbraD=AketbraC⋅ihB‾⋅ℎD
11 10 com13 ⊢A∈ℋ→B∈ℋ→C∈ℋ→D∈ℋ→C⋅ihB⋅ℎAketbraD=AketbraC⋅ihB‾⋅ℎD
12 11 imp43 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→C⋅ihB⋅ℎAketbraD=AketbraC⋅ihB‾⋅ℎD
13 bracl ⊢B∈ℋ∧C∈ℋ→bra⁡B⁡C∈ℂ
14 bracnln ⊢D∈ℋ→bra⁡D∈LinFn∩ContFn
15 cnvbramul ⊢bra⁡B⁡C∈ℂ∧bra⁡D∈LinFn∩ContFn→bra-1⁡bra⁡B⁡C·fnbra⁡D=bra⁡B⁡C‾⋅ℎbra-1⁡bra⁡D
16 13 14 15 syl2an ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→bra-1⁡bra⁡B⁡C·fnbra⁡D=bra⁡B⁡C‾⋅ℎbra-1⁡bra⁡D
17 braval ⊢B∈ℋ∧C∈ℋ→bra⁡B⁡C=C⋅ihB
18 17 fveq2d ⊢B∈ℋ∧C∈ℋ→bra⁡B⁡C‾=C⋅ihB‾
19 cnvbrabra ⊢D∈ℋ→bra-1⁡bra⁡D=D
20 18 19 oveqan12d ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→bra⁡B⁡C‾⋅ℎbra-1⁡bra⁡D=C⋅ihB‾⋅ℎD
21 16 20 eqtr2d ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→C⋅ihB‾⋅ℎD=bra-1⁡bra⁡B⁡C·fnbra⁡D
22 21 anasss ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→C⋅ihB‾⋅ℎD=bra-1⁡bra⁡B⁡C·fnbra⁡D
23 kbass2 ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→bra⁡B⁡C·fnbra⁡D=bra⁡B∘CketbraD
24 23 3expb ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→bra⁡B⁡C·fnbra⁡D=bra⁡B∘CketbraD
25 24 fveq2d ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→bra-1⁡bra⁡B⁡C·fnbra⁡D=bra-1⁡bra⁡B∘CketbraD
26 22 25 eqtr2d ⊢B∈ℋ∧C∈ℋ∧D∈ℋ→bra-1⁡bra⁡B∘CketbraD=C⋅ihB‾⋅ℎD
27 26 adantll ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→bra-1⁡bra⁡B∘CketbraD=C⋅ihB‾⋅ℎD
28 27 oveq2d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→Aketbrabra-1⁡bra⁡B∘CketbraD=AketbraC⋅ihB‾⋅ℎD
29 12 28 eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→C⋅ihB⋅ℎAketbraD=Aketbrabra-1⁡bra⁡B∘CketbraD
30 1 5 29 3eqtrd ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→AketbraB∘CketbraD=Aketbrabra-1⁡bra⁡B∘CketbraD