Metamath Proof Explorer

Theorem kbass6

Description: Dirac bra-ket associative law ( | A >. <. B | ) ( | C >. <. D | ) = | A >. ( <. B | ( | C >. <. D | ) ) . (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion kbass6 
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A ketbra B ) o. ( C ketbra D ) ) = ( A ketbra ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) ) )

Proof

Step Hyp Ref Expression
1 kbass5 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A ketbra B ) o. ( C ketbra D ) ) = ( ( ( A ketbra B ) ` C ) ketbra D ) )
2 kbval 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A ketbra B ) ` C ) = ( ( C .ih B ) .h A ) )
3 2 3expa 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A ketbra B ) ` C ) = ( ( C .ih B ) .h A ) )
4 3 adantrr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A ketbra B ) ` C ) = ( ( C .ih B ) .h A ) )
5 4 oveq1d 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A ketbra B ) ` C ) ketbra D ) = ( ( ( C .ih B ) .h A ) ketbra D ) )
6 hicl 
 |-  ( ( C e. ~H /\ B e. ~H ) -> ( C .ih B ) e. CC )
7 kbmul 
 |-  ( ( ( C .ih B ) e. CC /\ A e. ~H /\ D e. ~H ) -> ( ( ( C .ih B ) .h A ) ketbra D ) = ( A ketbra ( ( * ` ( C .ih B ) ) .h D ) ) )
8 6 7 syl3an1 
 |-  ( ( ( C e. ~H /\ B e. ~H ) /\ A e. ~H /\ D e. ~H ) -> ( ( ( C .ih B ) .h A ) ketbra D ) = ( A ketbra ( ( * ` ( C .ih B ) ) .h D ) ) )
9 8 3exp 
 |-  ( ( C e. ~H /\ B e. ~H ) -> ( A e. ~H -> ( D e. ~H -> ( ( ( C .ih B ) .h A ) ketbra D ) = ( A ketbra ( ( * ` ( C .ih B ) ) .h D ) ) ) ) )
10 9 ex 
 |-  ( C e. ~H -> ( B e. ~H -> ( A e. ~H -> ( D e. ~H -> ( ( ( C .ih B ) .h A ) ketbra D ) = ( A ketbra ( ( * ` ( C .ih B ) ) .h D ) ) ) ) ) )
11 10 com13 
 |-  ( A e. ~H -> ( B e. ~H -> ( C e. ~H -> ( D e. ~H -> ( ( ( C .ih B ) .h A ) ketbra D ) = ( A ketbra ( ( * ` ( C .ih B ) ) .h D ) ) ) ) ) )
12 11 imp43 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( C .ih B ) .h A ) ketbra D ) = ( A ketbra ( ( * ` ( C .ih B ) ) .h D ) ) )
13 bracl 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( bra ` B ) ` C ) e. CC )
14 bracnln 
 |-  ( D e. ~H -> ( bra ` D ) e. ( LinFn i^i ContFn ) )
15 cnvbramul 
 |-  ( ( ( ( bra ` B ) ` C ) e. CC /\ ( bra ` D ) e. ( LinFn i^i ContFn ) ) -> ( `' bra ` ( ( ( bra ` B ) ` C ) .fn ( bra ` D ) ) ) = ( ( * ` ( ( bra ` B ) ` C ) ) .h ( `' bra ` ( bra ` D ) ) ) )
16 13 14 15 syl2an 
 |-  ( ( ( B e. ~H /\ C e. ~H ) /\ D e. ~H ) -> ( `' bra ` ( ( ( bra ` B ) ` C ) .fn ( bra ` D ) ) ) = ( ( * ` ( ( bra ` B ) ` C ) ) .h ( `' bra ` ( bra ` D ) ) ) )
17 braval 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( bra ` B ) ` C ) = ( C .ih B ) )
18 17 fveq2d 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( * ` ( ( bra ` B ) ` C ) ) = ( * ` ( C .ih B ) ) )
19 cnvbrabra 
 |-  ( D e. ~H -> ( `' bra ` ( bra ` D ) ) = D )
20 18 19 oveqan12d 
 |-  ( ( ( B e. ~H /\ C e. ~H ) /\ D e. ~H ) -> ( ( * ` ( ( bra ` B ) ` C ) ) .h ( `' bra ` ( bra ` D ) ) ) = ( ( * ` ( C .ih B ) ) .h D ) )
21 16 20 eqtr2d 
 |-  ( ( ( B e. ~H /\ C e. ~H ) /\ D e. ~H ) -> ( ( * ` ( C .ih B ) ) .h D ) = ( `' bra ` ( ( ( bra ` B ) ` C ) .fn ( bra ` D ) ) ) )
22 21 anasss 
 |-  ( ( B e. ~H /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( * ` ( C .ih B ) ) .h D ) = ( `' bra ` ( ( ( bra ` B ) ` C ) .fn ( bra ` D ) ) ) )
23 kbass2 
 |-  ( ( B e. ~H /\ C e. ~H /\ D e. ~H ) -> ( ( ( bra ` B ) ` C ) .fn ( bra ` D ) ) = ( ( bra ` B ) o. ( C ketbra D ) ) )
24 23 3expb 
 |-  ( ( B e. ~H /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( bra ` B ) ` C ) .fn ( bra ` D ) ) = ( ( bra ` B ) o. ( C ketbra D ) ) )
25 24 fveq2d 
 |-  ( ( B e. ~H /\ ( C e. ~H /\ D e. ~H ) ) -> ( `' bra ` ( ( ( bra ` B ) ` C ) .fn ( bra ` D ) ) ) = ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) )
26 22 25 eqtr2d 
 |-  ( ( B e. ~H /\ ( C e. ~H /\ D e. ~H ) ) -> ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) = ( ( * ` ( C .ih B ) ) .h D ) )
27 26 adantll 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) = ( ( * ` ( C .ih B ) ) .h D ) )
28 27 oveq2d 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( A ketbra ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) ) = ( A ketbra ( ( * ` ( C .ih B ) ) .h D ) ) )
29 12 28 eqtr4d 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( C .ih B ) .h A ) ketbra D ) = ( A ketbra ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) ) )
30 1 5 29 3eqtrd 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A ketbra B ) o. ( C ketbra D ) ) = ( A ketbra ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) ) )