Metamath Proof Explorer

Theorem pjscji

Description: The projection of orthogonal subspaces is the sum of the projections. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjscji 
|- ( G C_ ( _|_ ` H ) -> ( projh ` ( G vH H ) ) = ( ( projh ` G ) +op ( projh ` H ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 pjcjt2 
 |-  ( ( G e. CH /\ H e. CH /\ x e. ~H ) -> ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G vH H ) ) ` x ) = ( ( ( projh ` G ) ` x ) +h ( ( projh ` H ) ` x ) ) ) )
4 1 2 3 mp3an12 
 |-  ( x e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G vH H ) ) ` x ) = ( ( ( projh ` G ) ` x ) +h ( ( projh ` H ) ` x ) ) ) )
5 4 impcom 
 |-  ( ( G C_ ( _|_ ` H ) /\ x e. ~H ) -> ( ( projh ` ( G vH H ) ) ` x ) = ( ( ( projh ` G ) ` x ) +h ( ( projh ` H ) ` x ) ) )
6 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
7 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
8 hosval 
 |-  ( ( ( projh ` G ) : ~H --> ~H /\ ( projh ` H ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( projh ` G ) +op ( projh ` H ) ) ` x ) = ( ( ( projh ` G ) ` x ) +h ( ( projh ` H ) ` x ) ) )
9 6 7 8 mp3an12 
 |-  ( x e. ~H -> ( ( ( projh ` G ) +op ( projh ` H ) ) ` x ) = ( ( ( projh ` G ) ` x ) +h ( ( projh ` H ) ` x ) ) )
10 9 adantl 
 |-  ( ( G C_ ( _|_ ` H ) /\ x e. ~H ) -> ( ( ( projh ` G ) +op ( projh ` H ) ) ` x ) = ( ( ( projh ` G ) ` x ) +h ( ( projh ` H ) ` x ) ) )
11 5 10 eqtr4d 
 |-  ( ( G C_ ( _|_ ` H ) /\ x e. ~H ) -> ( ( projh ` ( G vH H ) ) ` x ) = ( ( ( projh ` G ) +op ( projh ` H ) ) ` x ) )
12 11 ralrimiva 
 |-  ( G C_ ( _|_ ` H ) -> A. x e. ~H ( ( projh ` ( G vH H ) ) ` x ) = ( ( ( projh ` G ) +op ( projh ` H ) ) ` x ) )
13 1 2 chjcli 
 |-  ( G vH H ) e. CH
14 13 pjfi 
 |-  ( projh ` ( G vH H ) ) : ~H --> ~H
15 6 7 hoaddcli 
 |-  ( ( projh ` G ) +op ( projh ` H ) ) : ~H --> ~H
16 14 15 hoeqi 
 |-  ( A. x e. ~H ( ( projh ` ( G vH H ) ) ` x ) = ( ( ( projh ` G ) +op ( projh ` H ) ) ` x ) <-> ( projh ` ( G vH H ) ) = ( ( projh ` G ) +op ( projh ` H ) ) )
17 12 16 sylib 
 |-  ( G C_ ( _|_ ` H ) -> ( projh ` ( G vH H ) ) = ( ( projh ` G ) +op ( projh ` H ) ) )