Theorem 0leopj

Description: A projector is a positive operator. (Contributed by NM, 27-Sep-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	0leopj	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}T$$

Proof

Step	Hyp	Ref	Expression
1		elpjhmop	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to T\in \mathrm{HrmOp}$$
2		leopsq	$$⊢T\in \mathrm{HrmOp}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(T\circ T\right)$$
3	1 2	syl	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(T\circ T\right)$$
4		elpjidm	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to T\circ T=T$$
5	3 4	breqtrd	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}T$$