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	|- ( _I |` ~H ) e. LinOp

Proof

Step	Hyp	Ref	Expression
1		idunop	|- ( _I |` ~H ) e. UniOp
2		unoplin	|- ( ( _I |` ~H ) e. UniOp -> ( _I |` ~H ) e. LinOp )
3	1 2	ax-mp	|- ( _I |` ~H ) e. LinOp