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

Metamath Proof Explorer

Theorem kbfval

Description: The outer product of two vectors, expressed as | A >. <. B | in Dirac notation. See df-kb . (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Assertion kbfval 
|- ( ( A e. ~H /\ B e. ~H ) -> ( A ketbra B ) = ( x e. ~H |-> ( ( x .ih B ) .h A ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( y = A -> ( ( x .ih z ) .h y ) = ( ( x .ih z ) .h A ) )
2 1 mpteq2dv 
 |-  ( y = A -> ( x e. ~H |-> ( ( x .ih z ) .h y ) ) = ( x e. ~H |-> ( ( x .ih z ) .h A ) ) )
3 oveq2 
 |-  ( z = B -> ( x .ih z ) = ( x .ih B ) )
4 3 oveq1d 
 |-  ( z = B -> ( ( x .ih z ) .h A ) = ( ( x .ih B ) .h A ) )
5 4 mpteq2dv 
 |-  ( z = B -> ( x e. ~H |-> ( ( x .ih z ) .h A ) ) = ( x e. ~H |-> ( ( x .ih B ) .h A ) ) )
6 df-kb 
 |-  ketbra = ( y e. ~H , z e. ~H |-> ( x e. ~H |-> ( ( x .ih z ) .h y ) ) )
7 ax-hilex 
 |-  ~H e. _V
8 7 mptex 
 |-  ( x e. ~H |-> ( ( x .ih B ) .h A ) ) e. _V
9 2 5 6 8 ovmpo 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A ketbra B ) = ( x e. ~H |-> ( ( x .ih B ) .h A ) ) )