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	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A\mathrm{ketbra}B=\left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}B\right){\cdot }_{ℎ}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢y=A\to \left(x{\cdot }_{\mathrm{ih}}z\right){\cdot }_{ℎ}y=\left(x{\cdot }_{\mathrm{ih}}z\right){\cdot }_{ℎ}A$$
2	1	mpteq2dv	$$⊢y=A\to \left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}z\right){\cdot }_{ℎ}y\right)=\left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}z\right){\cdot }_{ℎ}A\right)$$
3		oveq2	$$⊢z=B\to x{\cdot }_{\mathrm{ih}}z=x{\cdot }_{\mathrm{ih}}B$$
4	3	oveq1d	$$⊢z=B\to \left(x{\cdot }_{\mathrm{ih}}z\right){\cdot }_{ℎ}A=\left(x{\cdot }_{\mathrm{ih}}B\right){\cdot }_{ℎ}A$$
5	4	mpteq2dv	$$⊢z=B\to \left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}z\right){\cdot }_{ℎ}A\right)=\left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}B\right){\cdot }_{ℎ}A\right)$$
6		df-kb	$$⊢\mathrm{ketbra}=\left(y\in \mathscr{H},z\in \mathscr{H}⟼\left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}z\right){\cdot }_{ℎ}y\right)\right)$$
7		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
8	7	mptex	$$⊢\left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}B\right){\cdot }_{ℎ}A\right)\in \mathrm{V}$$
9	2 5 6 8	ovmpo	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A\mathrm{ketbra}B=\left(x\in \mathscr{H}⟼\left(x{\cdot }_{\mathrm{ih}}B\right){\cdot }_{ℎ}A\right)$$