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 ) )