# 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$