Metamath Proof Explorer

Theorem kbass2

Description: Dirac bra-ket associative law ( <. A | B >. ) <. C | = <. A | ( | B >. <. C | ) , i.e., the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion kbass2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C = bra ⁡ A ∘ B ketbra C

Proof

Step Hyp Ref Expression
1 ovex ⊢ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x ∈ V
2 eqid ⊢ x ∈ ℋ ⟼ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x = x ∈ ℋ ⟼ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x
3 1 2 fnmpti ⊢ x ∈ ℋ ⟼ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x Fn ℋ
4 bracl ⊢ A ∈ ℋ ∧ B ∈ ℋ → bra ⁡ A ⁡ B ∈ ℂ
5 brafn ⊢ C ∈ ℋ → bra ⁡ C : ℋ ⟶ ℂ
6 hfmmval ⊢ bra ⁡ A ⁡ B ∈ ℂ ∧ bra ⁡ C : ℋ ⟶ ℂ → bra ⁡ A ⁡ B · fn bra ⁡ C = x ∈ ℋ ⟼ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x
7 4 5 6 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C = x ∈ ℋ ⟼ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x
8 7 3impa ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C = x ∈ ℋ ⟼ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x
9 8 fneq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C Fn ℋ ↔ x ∈ ℋ ⟼ bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x Fn ℋ
10 3 9 mpbiri ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C Fn ℋ
11 brafn ⊢ A ∈ ℋ → bra ⁡ A : ℋ ⟶ ℂ
12 kbop ⊢ B ∈ ℋ ∧ C ∈ ℋ → B ketbra C : ℋ ⟶ ℋ
13 fco ⊢ bra ⁡ A : ℋ ⟶ ℂ ∧ B ketbra C : ℋ ⟶ ℋ → bra ⁡ A ∘ B ketbra C : ℋ ⟶ ℂ
14 11 12 13 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ∘ B ketbra C : ℋ ⟶ ℂ
15 14 3impb ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ∘ B ketbra C : ℋ ⟶ ℂ
16 15 ffnd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ∘ B ketbra C Fn ℋ
17 simpl1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → A ∈ ℋ
18 simpl2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → B ∈ ℋ
19 braval ⊢ A ∈ ℋ ∧ B ∈ ℋ → bra ⁡ A ⁡ B = B ⋅ ih A
20 17 18 19 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ⁡ B = B ⋅ ih A
21 simpl3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → C ∈ ℋ
22 simpr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ∈ ℋ
23 braval ⊢ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ C ⁡ x = x ⋅ ih C
24 21 22 23 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ C ⁡ x = x ⋅ ih C
25 20 24 oveq12d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x = B ⋅ ih A ⁢ x ⋅ ih C
26 hicl ⊢ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A ∈ ℂ
27 18 17 26 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → B ⋅ ih A ∈ ℂ
28 20 27 eqeltrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ⁡ B ∈ ℂ
29 21 5 syl ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ C : ℋ ⟶ ℂ
30 hfmval ⊢ bra ⁡ A ⁡ B ∈ ℂ ∧ bra ⁡ C : ℋ ⟶ ℂ ∧ x ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C ⁡ x = bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x
31 28 29 22 30 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C ⁡ x = bra ⁡ A ⁡ B ⁢ bra ⁡ C ⁡ x
32 hicl ⊢ x ∈ ℋ ∧ C ∈ ℋ → x ⋅ ih C ∈ ℂ
33 22 21 32 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ∈ ℂ
34 ax-his3 ⊢ x ⋅ ih C ∈ ℂ ∧ B ∈ ℋ ∧ A ∈ ℋ → x ⋅ ih C ⋅ ℎ B ⋅ ih A = x ⋅ ih C ⁢ B ⋅ ih A
35 33 18 17 34 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ⋅ ℎ B ⋅ ih A = x ⋅ ih C ⁢ B ⋅ ih A
36 12 3adant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ketbra C : ℋ ⟶ ℋ
37 fvco3 ⊢ B ketbra C : ℋ ⟶ ℋ ∧ x ∈ ℋ → bra ⁡ A ∘ B ketbra C ⁡ x = bra ⁡ A ⁡ B ketbra C ⁡ x
38 36 37 sylan ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ∘ B ketbra C ⁡ x = bra ⁡ A ⁡ B ketbra C ⁡ x
39 kbval ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → B ketbra C ⁡ x = x ⋅ ih C ⋅ ℎ B
40 18 21 22 39 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → B ketbra C ⁡ x = x ⋅ ih C ⋅ ℎ B
41 40 fveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ⁡ B ketbra C ⁡ x = bra ⁡ A ⁡ x ⋅ ih C ⋅ ℎ B
42 hvmulcl ⊢ x ⋅ ih C ∈ ℂ ∧ B ∈ ℋ → x ⋅ ih C ⋅ ℎ B ∈ ℋ
43 33 18 42 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ⋅ ℎ B ∈ ℋ
44 braval ⊢ A ∈ ℋ ∧ x ⋅ ih C ⋅ ℎ B ∈ ℋ → bra ⁡ A ⁡ x ⋅ ih C ⋅ ℎ B = x ⋅ ih C ⋅ ℎ B ⋅ ih A
45 17 43 44 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ⁡ x ⋅ ih C ⋅ ℎ B = x ⋅ ih C ⋅ ℎ B ⋅ ih A
46 38 41 45 3eqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ∘ B ketbra C ⁡ x = x ⋅ ih C ⋅ ℎ B ⋅ ih A
47 27 33 mulcomd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → B ⋅ ih A ⁢ x ⋅ ih C = x ⋅ ih C ⁢ B ⋅ ih A
48 35 46 47 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ∘ B ketbra C ⁡ x = B ⋅ ih A ⁢ x ⋅ ih C
49 25 31 48 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C ⁡ x = bra ⁡ A ∘ B ketbra C ⁡ x
50 10 16 49 eqfnfvd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B · fn bra ⁡ C = bra ⁡ A ∘ B ketbra C