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