Metamath Proof Explorer

Theorem pjtoi

Description: Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis pjidmco.1 
|- H e. CH
Assertion pjtoi 
|- ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) = ( projh ` ~H )

Proof

Step Hyp Ref Expression
1 pjidmco.1 
 |-  H e. CH
2 axpjpj 
 |-  ( ( H e. CH /\ x e. ~H ) -> x = ( ( ( projh ` H ) ` x ) +h ( ( projh ` ( _|_ ` H ) ) ` x ) ) )
3 1 2 mpan 
 |-  ( x e. ~H -> x = ( ( ( projh ` H ) ` x ) +h ( ( projh ` ( _|_ ` H ) ) ` x ) ) )
4 pjch1 
 |-  ( x e. ~H -> ( ( projh ` ~H ) ` x ) = x )
5 1 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
6 1 choccli 
 |-  ( _|_ ` H ) e. CH
7 6 pjfi 
 |-  ( projh ` ( _|_ ` H ) ) : ~H --> ~H
8 hosval 
 |-  ( ( ( projh ` H ) : ~H --> ~H /\ ( projh ` ( _|_ ` H ) ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) ` x ) = ( ( ( projh ` H ) ` x ) +h ( ( projh ` ( _|_ ` H ) ) ` x ) ) )
9 5 7 8 mp3an12 
 |-  ( x e. ~H -> ( ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) ` x ) = ( ( ( projh ` H ) ` x ) +h ( ( projh ` ( _|_ ` H ) ) ` x ) ) )
10 3 4 9 3eqtr4rd 
 |-  ( x e. ~H -> ( ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) ` x ) = ( ( projh ` ~H ) ` x ) )
11 10 rgen 
 |-  A. x e. ~H ( ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) ` x ) = ( ( projh ` ~H ) ` x )
12 5 7 hoaddcli 
 |-  ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) : ~H --> ~H
13 helch 
 |-  ~H e. CH
14 13 pjfi 
 |-  ( projh ` ~H ) : ~H --> ~H
15 12 14 hoeqi 
 |-  ( A. x e. ~H ( ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) ` x ) = ( ( projh ` ~H ) ` x ) <-> ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) = ( projh ` ~H ) )
16 11 15 mpbi 
 |-  ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) = ( projh ` ~H )