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·fnbra⁡C=bra⁡A∘BketbraC

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⁡xFnℋ
4 bracl ⊢A∈ℋ∧B∈ℋ→bra⁡A⁡B∈ℂ
5 brafn ⊢C∈ℋ→bra⁡C:ℋ⟶ℂ
6 hfmmval ⊢bra⁡A⁡B∈ℂ∧bra⁡C:ℋ⟶ℂ→bra⁡A⁡B·fnbra⁡C=x∈ℋ⟼bra⁡A⁡B⁢bra⁡C⁡x
7 4 5 6 syl2an ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B·fnbra⁡C=x∈ℋ⟼bra⁡A⁡B⁢bra⁡C⁡x
8 7 3impa ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B·fnbra⁡C=x∈ℋ⟼bra⁡A⁡B⁢bra⁡C⁡x
9 8 fneq1d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B·fnbra⁡CFnℋ↔x∈ℋ⟼bra⁡A⁡B⁢bra⁡C⁡xFnℋ
10 3 9 mpbiri ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B·fnbra⁡CFnℋ
11 brafn ⊢A∈ℋ→bra⁡A:ℋ⟶ℂ
12 kbop ⊢B∈ℋ∧C∈ℋ→BketbraC:ℋ⟶ℋ
13 fco ⊢bra⁡A:ℋ⟶ℂ∧BketbraC:ℋ⟶ℋ→bra⁡A∘BketbraC:ℋ⟶ℂ
14 11 12 13 syl2an ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A∘BketbraC:ℋ⟶ℂ
15 14 3impb ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A∘BketbraC:ℋ⟶ℂ
16 15 ffnd ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A∘BketbraCFnℋ
17 simpl1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→A∈ℋ
18 simpl2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→B∈ℋ
19 braval ⊢A∈ℋ∧B∈ℋ→bra⁡A⁡B=B⋅ihA
20 17 18 19 syl2anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A⁡B=B⋅ihA
21 simpl3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→C∈ℋ
22 simpr ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x∈ℋ
23 braval ⊢C∈ℋ∧x∈ℋ→bra⁡C⁡x=x⋅ihC
24 21 22 23 syl2anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡C⁡x=x⋅ihC
25 20 24 oveq12d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A⁡B⁢bra⁡C⁡x=B⋅ihA⁢x⋅ihC
26 hicl ⊢B∈ℋ∧A∈ℋ→B⋅ihA∈ℂ
27 18 17 26 syl2anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→B⋅ihA∈ℂ
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·fnbra⁡C⁡x=bra⁡A⁡B⁢bra⁡C⁡x
31 28 29 22 30 syl3anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A⁡B·fnbra⁡C⁡x=bra⁡A⁡B⁢bra⁡C⁡x
32 hicl ⊢x∈ℋ∧C∈ℋ→x⋅ihC∈ℂ
33 22 21 32 syl2anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC∈ℂ
34 ax-his3 ⊢x⋅ihC∈ℂ∧B∈ℋ∧A∈ℋ→x⋅ihC⋅ℎB⋅ihA=x⋅ihC⁢B⋅ihA
35 33 18 17 34 syl3anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC⋅ℎB⋅ihA=x⋅ihC⁢B⋅ihA
36 12 3adant1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→BketbraC:ℋ⟶ℋ
37 fvco3 ⊢BketbraC:ℋ⟶ℋ∧x∈ℋ→bra⁡A∘BketbraC⁡x=bra⁡A⁡BketbraC⁡x
38 36 37 sylan ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A∘BketbraC⁡x=bra⁡A⁡BketbraC⁡x
39 kbval ⊢B∈ℋ∧C∈ℋ∧x∈ℋ→BketbraC⁡x=x⋅ihC⋅ℎB
40 18 21 22 39 syl3anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→BketbraC⁡x=x⋅ihC⋅ℎB
41 40 fveq2d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A⁡BketbraC⁡x=bra⁡A⁡x⋅ihC⋅ℎB
42 hvmulcl ⊢x⋅ihC∈ℂ∧B∈ℋ→x⋅ihC⋅ℎB∈ℋ
43 33 18 42 syl2anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC⋅ℎB∈ℋ
44 braval ⊢A∈ℋ∧x⋅ihC⋅ℎB∈ℋ→bra⁡A⁡x⋅ihC⋅ℎB=x⋅ihC⋅ℎB⋅ihA
45 17 43 44 syl2anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A⁡x⋅ihC⋅ℎB=x⋅ihC⋅ℎB⋅ihA
46 38 41 45 3eqtrd ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A∘BketbraC⁡x=x⋅ihC⋅ℎB⋅ihA
47 27 33 mulcomd ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→B⋅ihA⁢x⋅ihC=x⋅ihC⁢B⋅ihA
48 35 46 47 3eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A∘BketbraC⁡x=B⋅ihA⁢x⋅ihC
49 25 31 48 3eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧x∈ℋ→bra⁡A⁡B·fnbra⁡C⁡x=bra⁡A∘BketbraC⁡x
50 10 16 49 eqfnfvd ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B·fnbra⁡C=bra⁡A∘BketbraC