Theorem lnopfi

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

	Ref	Expression
Hypothesis	lnopl.1	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		lnopl.1	$$⊢T\in \mathrm{LinOp}$$
2		lnopf	$$⊢T\in \mathrm{LinOp}\to T:\mathscr{H}⟶\mathscr{H}$$
3	1 2	ax-mp	$$⊢T:\mathscr{H}⟶\mathscr{H}$$