This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjo

Description: The orthogonal projection. Lemma 4.4(i) of Beran p. 111. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjch1 
 |-  ( A e. ~H -> ( ( projh ` ~H ) ` A ) = A )
2 1 adantl 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ~H ) ` A ) = A )
3 axpjpj 
 |-  ( ( H e. CH /\ A e. ~H ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
4 2 3 eqtr2d 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( projh ` ~H ) ` A ) )
5 helch 
 |-  ~H e. CH
6 5 pjcli 
 |-  ( A e. ~H -> ( ( projh ` ~H ) ` A ) e. ~H )
7 6 adantl 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ~H ) ` A ) e. ~H )
8 pjhcl 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ~H )
9 choccl 
 |-  ( H e. CH -> ( _|_ ` H ) e. CH )
10 pjhcl 
 |-  ( ( ( _|_ ` H ) e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H )
11 9 10 sylan 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H )
12 hvsubadd 
 |-  ( ( ( ( projh ` ~H ) ` A ) e. ~H /\ ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H ) -> ( ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( _|_ ` H ) ) ` A ) <-> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( projh ` ~H ) ` A ) ) )
13 7 8 11 12 syl3anc 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( _|_ ` H ) ) ` A ) <-> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( projh ` ~H ) ` A ) ) )
14 4 13 mpbird 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( _|_ ` H ) ) ` A ) )
15 14 eqcomd 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` H ) ` A ) ) )