Description: Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pjpj.1 | |- H e. CH |
|
pjpj.2 | |- A e. ~H |
||
Assertion | pjpji | |- A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjpj.1 | |- H e. CH |
|
2 | pjpj.2 | |- A e. ~H |
|
3 | 1 2 | pjpj0i | |- A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) |