# 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 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}\mathrm{ketbra}{B}\right):ℋ⟶ℋ$

### Proof

Step Hyp Ref Expression
1 kbfval ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}\mathrm{ketbra}{B}=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)$
2 hicl ${⊢}\left({x}\in ℋ\wedge {B}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
3 hvmulcl ${⊢}\left({x}{\cdot }_{\mathrm{ih}}{B}\in ℂ\wedge {A}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\in ℋ$
4 2 3 sylan ${⊢}\left(\left({x}\in ℋ\wedge {B}\in ℋ\right)\wedge {A}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\in ℋ$
5 4 an31s ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\in ℋ$
6 1 5 fmpt3d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}\mathrm{ketbra}{B}\right):ℋ⟶ℋ$