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	⊢ ( 𝐻 ∈ Cℋ → ( adjℎ ‘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		pjmfn	⊢ projℎ Fn Cℋ
2		fnfvelrn	⊢ ( ( projℎ Fn Cℋ ∧ 𝐻 ∈ Cℋ ) → ( projℎ ‘ 𝐻 ) ∈ ran projℎ )
3	1 2	mpan	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) ∈ ran projℎ )
4		pjadj2	⊢ ( ( projℎ ‘ 𝐻 ) ∈ ran projℎ → ( adjℎ ‘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) )
5	3 4	syl	⊢ ( 𝐻 ∈ Cℋ → ( adjℎ ‘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) )