Theorem idlnop

Description: The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	idlnop	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{LinOp}$$

Proof

Step	Hyp	Ref	Expression
1		idunop	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{UniOp}$$
2		unoplin	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{UniOp}\to {\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{LinOp}$$
3	1 2	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{LinOp}$$