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 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ketbra B : ℋ ⟶ ℋ

Proof

Step Hyp Ref Expression
1 kbfval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ketbra B = x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A
2 hicl ⊢ x ∈ ℋ ∧ B ∈ ℋ → x ⋅ ih B ∈ ℂ
3 hvmulcl ⊢ x ⋅ ih B ∈ ℂ ∧ A ∈ ℋ → x ⋅ ih B ⋅ ℎ A ∈ ℋ
4 2 3 sylan ⊢ x ∈ ℋ ∧ B ∈ ℋ ∧ A ∈ ℋ → x ⋅ ih B ⋅ ℎ A ∈ ℋ
5 4 an31s ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih B ⋅ ℎ A ∈ ℋ
6 1 5 fmpt3d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ketbra B : ℋ ⟶ ℋ