Metamath Proof Explorer

Theorem kbass4

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 kbass4 
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) = ( ( bra ` A ) ` ( ( ( bra ` C ) ` D ) .h B ) ) )

Proof

Step Hyp Ref Expression
1 bracl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) e. CC )
2 bracl 
 |-  ( ( C e. ~H /\ D e. ~H ) -> ( ( bra ` C ) ` D ) e. CC )
3 mulcom 
 |-  ( ( ( ( bra ` A ) ` B ) e. CC /\ ( ( bra ` C ) ` D ) e. CC ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) = ( ( ( bra ` C ) ` D ) x. ( ( bra ` A ) ` B ) ) )
4 1 2 3 syl2an 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) = ( ( ( bra ` C ) ` D ) x. ( ( bra ` A ) ` B ) ) )
5 bralnfn 
 |-  ( A e. ~H -> ( bra ` A ) e. LinFn )
6 5 ad2antrr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( bra ` A ) e. LinFn )
7 2 adantl 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( bra ` C ) ` D ) e. CC )
8 simplr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> B e. ~H )
9 lnfnmul 
 |-  ( ( ( bra ` A ) e. LinFn /\ ( ( bra ` C ) ` D ) e. CC /\ B e. ~H ) -> ( ( bra ` A ) ` ( ( ( bra ` C ) ` D ) .h B ) ) = ( ( ( bra ` C ) ` D ) x. ( ( bra ` A ) ` B ) ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( bra ` A ) ` ( ( ( bra ` C ) ` D ) .h B ) ) = ( ( ( bra ` C ) ` D ) x. ( ( bra ` A ) ` B ) ) )
11 4 10 eqtr4d 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) = ( ( bra ` A ) ` ( ( ( bra ` C ) ` D ) .h B ) ) )