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