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

Metamath Proof Explorer

Theorem kbass3

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

Proof

Step Hyp Ref Expression
1 bracl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) e. CC )
2 1 adantr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( bra ` A ) ` B ) e. CC )
3 brafn 
 |-  ( C e. ~H -> ( bra ` C ) : ~H --> CC )
4 3 ad2antrl 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( bra ` C ) : ~H --> CC )
5 simprr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> D e. ~H )
6 hfmval 
 |-  ( ( ( ( bra ` A ) ` B ) e. CC /\ ( bra ` C ) : ~H --> CC /\ D e. ~H ) -> ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) ` D ) = ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) )
7 2 4 5 6 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) ` D ) = ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) )
8 7 eqcomd 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) = ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) ` D ) )