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