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 ↾ ℋ ) ∈ LinOp

Proof

Step	Hyp	Ref	Expression
1		idunop	⊢ ( I ↾ ℋ ) ∈ UniOp
2		unoplin	⊢ ( ( I ↾ ℋ ) ∈ UniOp → ( I ↾ ℋ ) ∈ LinOp )
3	1 2	ax-mp	⊢ ( I ↾ ℋ ) ∈ LinOp