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:\mathscr{H}⟶\mathscr{H}\right)\to \left(A{·}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$

Proof

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