# Metamath Proof Explorer

## Theorem homulcl

Description: The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$

### Proof

Step Hyp Ref Expression
1 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
2 hvmulcl ${⊢}\left({A}\in ℂ\wedge {T}\left({x}\right)\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left({x}\right)\in ℋ$
3 1 2 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\right)\to {A}{\cdot }_{ℎ}{T}\left({x}\right)\in ℋ$
4 3 anassrs ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left({x}\right)\in ℋ$
5 4 fmpttd ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right):ℋ⟶ℋ$
6 hommval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right)$
7 6 feq1d ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ↔\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right):ℋ⟶ℋ\right)$
8 5 7 mpbird ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$