Metamath Proof Explorer


Theorem pjoccl

Description: The part of a vector that belongs to the orthocomplemented space. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjoccl
|- ( ( H e. CH /\ A e. ~H ) -> ( A -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) )

Proof

Step Hyp Ref Expression
1 pjop
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) = ( A -h ( ( projh ` H ) ` A ) ) )
2 choccl
 |-  ( H e. CH -> ( _|_ ` H ) e. CH )
3 axpjcl
 |-  ( ( ( _|_ ` H ) e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) )
4 2 3 sylan
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) )
5 1 4 eqeltrrd
 |-  ( ( H e. CH /\ A e. ~H ) -> ( A -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) )