Metamath Proof Explorer

Theorem 0leopj

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

Ref Expression
Assertion 0leopj 
|- ( T e. ran projh -> 0hop <_op T )

Proof

Step Hyp Ref Expression
1 elpjhmop 
 |-  ( T e. ran projh -> T e. HrmOp )
2 leopsq 
 |-  ( T e. HrmOp -> 0hop <_op ( T o. T ) )
3 1 2 syl 
 |-  ( T e. ran projh -> 0hop <_op ( T o. T ) )
4 elpjidm 
 |-  ( T e. ran projh -> ( T o. T ) = T )
5 3 4 breqtrd 
 |-  ( T e. ran projh -> 0hop <_op T )