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

Metamath Proof Explorer

Theorem kbop

Description: The outer product of two vectors, expressed as | A >. <. B | in Dirac notation, is an operator. (Contributed by NM, 30-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion kbop 
|- ( ( A e. ~H /\ B e. ~H ) -> ( A ketbra B ) : ~H --> ~H )

Proof

Step Hyp Ref Expression
1 kbfval 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A ketbra B ) = ( x e. ~H |-> ( ( x .ih B ) .h A ) ) )
2 hicl 
 |-  ( ( x e. ~H /\ B e. ~H ) -> ( x .ih B ) e. CC )
3 hvmulcl 
 |-  ( ( ( x .ih B ) e. CC /\ A e. ~H ) -> ( ( x .ih B ) .h A ) e. ~H )
4 2 3 sylan 
 |-  ( ( ( x e. ~H /\ B e. ~H ) /\ A e. ~H ) -> ( ( x .ih B ) .h A ) e. ~H )
5 4 an31s 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ~H ) -> ( ( x .ih B ) .h A ) e. ~H )
6 1 5 fmpt3d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A ketbra B ) : ~H --> ~H )