Theorem pjpoi

Description: Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjop.1	|- H e. CH
	pjop.2	|- A e. ~H
Assertion	pjpoi	|- ( ( projh ` H ) ` A ) = ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		pjop.1	|- H e. CH
2		pjop.2	|- A e. ~H
3		pjpo	|- ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) = ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
4	1 2 3	mp2an	|- ( ( projh ` H ) ` A ) = ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) )