Metamath Proof Explorer

Theorem pjadj2

Description: A projector is self-adjoint. Property (i) of Beran p. 109. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion pjadj2 
|- ( T e. ran projh -> ( adjh ` T ) = T )

Proof

Step Hyp Ref Expression
1 elpjhmop 
 |-  ( T e. ran projh -> T e. HrmOp )
2 hmopadj 
 |-  ( T e. HrmOp -> ( adjh ` T ) = T )
3 1 2 syl 
 |-  ( T e. ran projh -> ( adjh ` T ) = T )