Theorem pjlnopi

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

	Ref	Expression
Hypothesis	pjhmop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjlnopi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{LinOp}$$

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	pjhmopi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{HrmOp}$$
3		hmoplin	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{HrmOp}\to {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{LinOp}$$
4	2 3	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{LinOp}$$