Theorem lnopf

Description: A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	lnopf	$$⊢T\in \mathrm{LinOp}\to T:\mathscr{H}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		ellnop	$$⊢T\in \mathrm{LinOp}\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in ℂ\forall y\in \mathscr{H}\forall z\in \mathscr{H}T\left(\left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\right)=\left(x{\cdot }_{ℎ}T\left(y\right)\right){+}_{ℎ}T\left(z\right)\right)$$
2	1	simplbi	$$⊢T\in \mathrm{LinOp}\to T:\mathscr{H}⟶\mathscr{H}$$