This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ·fn ( bra ‘ 𝐶 ) ) = ( ( bra ‘ 𝐴 ) ∘ ( 𝐵 ketbra 𝐶 ) ) )

Proof

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