Metamath Proof Explorer


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 ) )