Metamath Proof Explorer

Theorem pjpo

Description: Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjpo 
|- ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) = ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 choccl 
 |-  ( H e. CH -> ( _|_ ` H ) e. CH )
2 pjhcl 
 |-  ( ( ( _|_ ` H ) e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H )
3 1 2 sylan 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H )
4 pjhcl 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ~H )
5 ax-hvcom 
 |-  ( ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H /\ ( ( projh ` H ) ` A ) e. ~H ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
6 3 4 5 syl2anc 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
7 axpjpj 
 |-  ( ( H e. CH /\ A e. ~H ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
8 6 7 eqtr4d 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = A )
9 simpr 
 |-  ( ( H e. CH /\ A e. ~H ) -> A e. ~H )
10 hvsubadd 
 |-  ( ( A e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H /\ ( ( projh ` H ) ` A ) e. ~H ) -> ( ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( projh ` H ) ` A ) <-> ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = A ) )
11 9 3 4 10 syl3anc 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( projh ` H ) ` A ) <-> ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = A ) )
12 8 11 mpbird 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( projh ` H ) ` A ) )
13 12 eqcomd 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) = ( A -h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )