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 | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ketbra 𝐵 ) : ℋ ⟶ ℋ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | kbfval | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ketbra 𝐵 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih 𝐵 ) ·ℎ 𝐴 ) ) ) | |
| 2 | hicl | ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ·ih 𝐵 ) ∈ ℂ ) | |
| 3 | hvmulcl | ⊢ ( ( ( 𝑥 ·ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐵 ) ·ℎ 𝐴 ) ∈ ℋ ) | |
| 4 | 2 3 | sylan | ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐴 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐵 ) ·ℎ 𝐴 ) ∈ ℋ ) |
| 5 | 4 | an31s | ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐵 ) ·ℎ 𝐴 ) ∈ ℋ ) |
| 6 | 1 5 | fmpt3d | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ketbra 𝐵 ) : ℋ ⟶ ℋ ) |