Theorem lnopmuli

Description: Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnopl.1	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnopmuli	$$⊢\left(A\in ℂ\wedge B\in \mathscr{H}\right)\to T\left(A{\cdot }_{ℎ}B\right)=A{\cdot }_{ℎ}T\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		lnopl.1	$$⊢T\in \mathrm{LinOp}$$
2		lnopmul	$$⊢\left(T\in \mathrm{LinOp}\wedge A\in ℂ\wedge B\in \mathscr{H}\right)\to T\left(A{\cdot }_{ℎ}B\right)=A{\cdot }_{ℎ}T\left(B\right)$$
3	1 2	mp3an1	$$⊢\left(A\in ℂ\wedge B\in \mathscr{H}\right)\to T\left(A{\cdot }_{ℎ}B\right)=A{\cdot }_{ℎ}T\left(B\right)$$