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 TranprojadjhT=T

Proof

Step Hyp Ref Expression
1 elpjhmop TranprojTHrmOp
2 hmopadj THrmOpadjhT=T
3 1 2 syl TranprojadjhT=T