Metamath Proof Explorer


Theorem axpjpj

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

Proof

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