Metamath Proof Explorer


Theorem pjadj3

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

Ref Expression
Assertion pjadj3 HCadjhprojH=projH

Proof

Step Hyp Ref Expression
1 pjmfn projFnC
2 fnfvelrn projFnCHCprojHranproj
3 1 2 mpan HCprojHranproj
4 pjadj2 projHranprojadjhprojH=projH
5 3 4 syl HCadjhprojH=projH