Theorem pjvec

Description: The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjvec	|- ( H e. CH -> H = { x e. ~H | ( ( projh ` H ) ` x ) = x } )

Proof

Step	Hyp	Ref	Expression
1		chss	|- ( H e. CH -> H C_ ~H )
2		sseqin2	|- ( H C_ ~H <-> ( ~H i^i H ) = H )
3	1 2	sylib	|- ( H e. CH -> ( ~H i^i H ) = H )
4		pjch	|- ( ( H e. CH /\ x e. ~H ) -> ( x e. H <-> ( ( projh ` H ) ` x ) = x ) )
5	4	rabbi2dva	|- ( H e. CH -> ( ~H i^i H ) = { x e. ~H | ( ( projh ` H ) ` x ) = x } )
6	3 5	eqtr3d	|- ( H e. CH -> H = { x e. ~H | ( ( projh ` H ) ` x ) = x } )