Theorem pjlnopi

Description: A projector is a linear operator. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjhmop.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjlnopi	⊢ ( projℎ ‘ 𝐻 ) ∈ LinOp

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	⊢ 𝐻 ∈ Cℋ
2	1	pjhmopi	⊢ ( projℎ ‘ 𝐻 ) ∈ HrmOp
3		hmoplin	⊢ ( ( projℎ ‘ 𝐻 ) ∈ HrmOp → ( projℎ ‘ 𝐻 ) ∈ LinOp )
4	2 3	ax-mp	⊢ ( projℎ ‘ 𝐻 ) ∈ LinOp