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	|- ( H e. CH -> ( adjh ` ( projh ` H ) ) = ( projh ` H ) )

Proof

Step	Hyp	Ref	Expression
1		pjmfn	|- projh Fn CH
2		fnfvelrn	|- ( ( projh Fn CH /\ H e. CH ) -> ( projh ` H ) e. ran projh )
3	1 2	mpan	|- ( H e. CH -> ( projh ` H ) e. ran projh )
4		pjadj2	|- ( ( projh ` H ) e. ran projh -> ( adjh ` ( projh ` H ) ) = ( projh ` H ) )
5	3 4	syl	|- ( H e. CH -> ( adjh ` ( projh ` H ) ) = ( projh ` H ) )