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\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {adj}_h\left(T\right)=T$$

Proof

Step	Hyp	Ref	Expression
1		elpjhmop	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to T\in \mathrm{HrmOp}$$
2		hmopadj	$$⊢T\in \mathrm{HrmOp}\to {adj}_h\left(T\right)=T$$
3	1 2	syl	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {adj}_h\left(T\right)=T$$