Description: Decomposition of a vector into projections. See comment in axpjcl . (Contributed by NM, 26-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | axpjpj | |- ( ( H e. CH /\ A e. ~H ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |- ( ( H e. CH /\ A e. ~H ) -> H e. CH ) |
|
2 | pjhth | |- ( H e. CH -> ( H +H ( _|_ ` H ) ) = ~H ) |
|
3 | 2 | eleq2d | |- ( H e. CH -> ( A e. ( H +H ( _|_ ` H ) ) <-> A e. ~H ) ) |
4 | 3 | biimpar | |- ( ( H e. CH /\ A e. ~H ) -> A e. ( H +H ( _|_ ` H ) ) ) |
5 | 1 4 | pjpjpre | |- ( ( H e. CH /\ A e. ~H ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) |