Metamath Proof Explorer


Theorem pjpji

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

Proof

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