Theorem pjopi

Description: Orthocomplement projection in terms of 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	pjopi	|- ( ( 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		pjop	|- ( ( 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 ) )