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 e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) = ( ( bra ` A ) o. ( B ketbra C ) ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) e. _V
2 eqid 
 |-  ( x e. ~H |-> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) ) = ( x e. ~H |-> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) )
3 1 2 fnmpti 
 |-  ( x e. ~H |-> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) ) Fn ~H
4 bracl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) e. CC )
5 brafn 
 |-  ( C e. ~H -> ( bra ` C ) : ~H --> CC )
6 hfmmval 
 |-  ( ( ( ( bra ` A ) ` B ) e. CC /\ ( bra ` C ) : ~H --> CC ) -> ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) = ( x e. ~H |-> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) ) )
7 4 5 6 syl2an 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) = ( x e. ~H |-> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) ) )
8 7 3impa 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) = ( x e. ~H |-> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) ) )
9 8 fneq1d 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) Fn ~H <-> ( x e. ~H |-> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) ) Fn ~H ) )
10 3 9 mpbiri 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) Fn ~H )
11 brafn 
 |-  ( A e. ~H -> ( bra ` A ) : ~H --> CC )
12 kbop 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( B ketbra C ) : ~H --> ~H )
13 fco 
 |-  ( ( ( bra ` A ) : ~H --> CC /\ ( B ketbra C ) : ~H --> ~H ) -> ( ( bra ` A ) o. ( B ketbra C ) ) : ~H --> CC )
14 11 12 13 syl2an 
 |-  ( ( A e. ~H /\ ( B e. ~H /\ C e. ~H ) ) -> ( ( bra ` A ) o. ( B ketbra C ) ) : ~H --> CC )
15 14 3impb 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( bra ` A ) o. ( B ketbra C ) ) : ~H --> CC )
16 15 ffnd 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( bra ` A ) o. ( B ketbra C ) ) Fn ~H )
17 simpl1 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> A e. ~H )
18 simpl2 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> B e. ~H )
19 braval 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) = ( B .ih A ) )
20 17 18 19 syl2anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( bra ` A ) ` B ) = ( B .ih A ) )
21 simpl3 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> C e. ~H )
22 simpr 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> x e. ~H )
23 braval 
 |-  ( ( C e. ~H /\ x e. ~H ) -> ( ( bra ` C ) ` x ) = ( x .ih C ) )
24 21 22 23 syl2anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( bra ` C ) ` x ) = ( x .ih C ) )
25 20 24 oveq12d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) = ( ( B .ih A ) x. ( x .ih C ) ) )
26 hicl 
 |-  ( ( B e. ~H /\ A e. ~H ) -> ( B .ih A ) e. CC )
27 18 17 26 syl2anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( B .ih A ) e. CC )
28 20 27 eqeltrd 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( bra ` A ) ` B ) e. CC )
29 21 5 syl 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( bra ` C ) : ~H --> CC )
30 hfmval 
 |-  ( ( ( ( bra ` A ) ` B ) e. CC /\ ( bra ` C ) : ~H --> CC /\ x e. ~H ) -> ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) ` x ) = ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) )
31 28 29 22 30 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) ` x ) = ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` x ) ) )
32 hicl 
 |-  ( ( x e. ~H /\ C e. ~H ) -> ( x .ih C ) e. CC )
33 22 21 32 syl2anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( x .ih C ) e. CC )
34 ax-his3 
 |-  ( ( ( x .ih C ) e. CC /\ B e. ~H /\ A e. ~H ) -> ( ( ( x .ih C ) .h B ) .ih A ) = ( ( x .ih C ) x. ( B .ih A ) ) )
35 33 18 17 34 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( x .ih C ) .h B ) .ih A ) = ( ( x .ih C ) x. ( B .ih A ) ) )
36 12 3adant1 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( B ketbra C ) : ~H --> ~H )
37 fvco3 
 |-  ( ( ( B ketbra C ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( bra ` A ) o. ( B ketbra C ) ) ` x ) = ( ( bra ` A ) ` ( ( B ketbra C ) ` x ) ) )
38 36 37 sylan 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( bra ` A ) o. ( B ketbra C ) ) ` x ) = ( ( bra ` A ) ` ( ( B ketbra C ) ` x ) ) )
39 kbval 
 |-  ( ( B e. ~H /\ C e. ~H /\ x e. ~H ) -> ( ( B ketbra C ) ` x ) = ( ( x .ih C ) .h B ) )
40 18 21 22 39 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( B ketbra C ) ` x ) = ( ( x .ih C ) .h B ) )
41 40 fveq2d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( bra ` A ) ` ( ( B ketbra C ) ` x ) ) = ( ( bra ` A ) ` ( ( x .ih C ) .h B ) ) )
42 hvmulcl 
 |-  ( ( ( x .ih C ) e. CC /\ B e. ~H ) -> ( ( x .ih C ) .h B ) e. ~H )
43 33 18 42 syl2anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( x .ih C ) .h B ) e. ~H )
44 braval 
 |-  ( ( A e. ~H /\ ( ( x .ih C ) .h B ) e. ~H ) -> ( ( bra ` A ) ` ( ( x .ih C ) .h B ) ) = ( ( ( x .ih C ) .h B ) .ih A ) )
45 17 43 44 syl2anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( bra ` A ) ` ( ( x .ih C ) .h B ) ) = ( ( ( x .ih C ) .h B ) .ih A ) )
46 38 41 45 3eqtrd 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( bra ` A ) o. ( B ketbra C ) ) ` x ) = ( ( ( x .ih C ) .h B ) .ih A ) )
47 27 33 mulcomd 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( B .ih A ) x. ( x .ih C ) ) = ( ( x .ih C ) x. ( B .ih A ) ) )
48 35 46 47 3eqtr4d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( bra ` A ) o. ( B ketbra C ) ) ` x ) = ( ( B .ih A ) x. ( x .ih C ) ) )
49 25 31 48 3eqtr4d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) ` x ) = ( ( ( bra ` A ) o. ( B ketbra C ) ) ` x ) )
50 10 16 49 eqfnfvd 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) = ( ( bra ` A ) o. ( B ketbra C ) ) )