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	⊢ ( 𝑇 ∈ ran projℎ → ( adjℎ ‘ 𝑇 ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		elpjhmop	⊢ ( 𝑇 ∈ ran projℎ → 𝑇 ∈ HrmOp )
2		hmopadj	⊢ ( 𝑇 ∈ HrmOp → ( adjℎ ‘ 𝑇 ) = 𝑇 )
3	1 2	syl	⊢ ( 𝑇 ∈ ran projℎ → ( adjℎ ‘ 𝑇 ) = 𝑇 )