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 ∈ ℋ → A ketbra B ∘ C ketbra D = A ketbra bra -1 ⁡ bra ⁡ B ∘ C ketbra D

Proof

Step Hyp Ref Expression
1 kbass5 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ketbra B ∘ C ketbra D = A ketbra B ⁡ C ketbra D
2 kbval ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ketbra B ⁡ C = C ⋅ ih B ⋅ ℎ A
3 2 3expa ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ketbra B ⁡ C = C ⋅ ih B ⋅ ℎ A
4 3 adantrr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ketbra B ⁡ C = C ⋅ ih B ⋅ ℎ A
5 4 oveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ketbra B ⁡ C ketbra D = C ⋅ ih B ⋅ ℎ A ketbra D
6 hicl ⊢ C ∈ ℋ ∧ B ∈ ℋ → C ⋅ ih B ∈ ℂ
7 kbmul ⊢ C ⋅ ih B ∈ ℂ ∧ A ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ⋅ ℎ A ketbra D = A ketbra C ⋅ ih B ‾ ⋅ ℎ D
8 6 7 syl3an1 ⊢ C ∈ ℋ ∧ B ∈ ℋ ∧ A ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ⋅ ℎ A ketbra D = A ketbra C ⋅ ih B ‾ ⋅ ℎ D
9 8 3exp ⊢ C ∈ ℋ ∧ B ∈ ℋ → A ∈ ℋ → D ∈ ℋ → C ⋅ ih B ⋅ ℎ A ketbra D = A ketbra C ⋅ ih B ‾ ⋅ ℎ D
10 9 ex ⊢ C ∈ ℋ → B ∈ ℋ → A ∈ ℋ → D ∈ ℋ → C ⋅ ih B ⋅ ℎ A ketbra D = A ketbra C ⋅ ih B ‾ ⋅ ℎ D
11 10 com13 ⊢ A ∈ ℋ → B ∈ ℋ → C ∈ ℋ → D ∈ ℋ → C ⋅ ih B ⋅ ℎ A ketbra D = A ketbra C ⋅ ih B ‾ ⋅ ℎ D
12 11 imp43 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ⋅ ℎ A ketbra D = A ketbra C ⋅ ih B ‾ ⋅ ℎ 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 · fn bra ⁡ D = bra ⁡ B ⁡ C ‾ ⋅ ℎ bra -1 ⁡ bra ⁡ D
16 13 14 15 syl2an ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra -1 ⁡ bra ⁡ B ⁡ C · fn bra ⁡ D = bra ⁡ B ⁡ C ‾ ⋅ ℎ bra -1 ⁡ bra ⁡ D
17 braval ⊢ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ B ⁡ C = C ⋅ ih B
18 17 fveq2d ⊢ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ B ⁡ C ‾ = C ⋅ ih B ‾
19 cnvbrabra ⊢ D ∈ ℋ → bra -1 ⁡ bra ⁡ D = D
20 18 19 oveqan12d ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ B ⁡ C ‾ ⋅ ℎ bra -1 ⁡ bra ⁡ D = C ⋅ ih B ‾ ⋅ ℎ D
21 16 20 eqtr2d ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ‾ ⋅ ℎ D = bra -1 ⁡ bra ⁡ B ⁡ C · fn bra ⁡ D
22 21 anasss ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ‾ ⋅ ℎ D = bra -1 ⁡ bra ⁡ B ⁡ C · fn bra ⁡ D
23 kbass2 ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ B ⁡ C · fn bra ⁡ D = bra ⁡ B ∘ C ketbra D
24 23 3expb ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra ⁡ B ⁡ C · fn bra ⁡ D = bra ⁡ B ∘ C ketbra D
25 24 fveq2d ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra -1 ⁡ bra ⁡ B ⁡ C · fn bra ⁡ D = bra -1 ⁡ bra ⁡ B ∘ C ketbra D
26 22 25 eqtr2d ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra -1 ⁡ bra ⁡ B ∘ C ketbra D = C ⋅ ih B ‾ ⋅ ℎ D
27 26 adantll ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → bra -1 ⁡ bra ⁡ B ∘ C ketbra D = C ⋅ ih B ‾ ⋅ ℎ D
28 27 oveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ketbra bra -1 ⁡ bra ⁡ B ∘ C ketbra D = A ketbra C ⋅ ih B ‾ ⋅ ℎ D
29 12 28 eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ⋅ ℎ A ketbra D = A ketbra bra -1 ⁡ bra ⁡ B ∘ C ketbra D
30 1 5 29 3eqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ketbra B ∘ C ketbra D = A ketbra bra -1 ⁡ bra ⁡ B ∘ C ketbra D