Metamath Proof Explorer

Theorem pjds3i

Description: Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjds3.1 
|- F e. CH
pjds3.2 
|- G e. CH
pjds3.3 
|- H e. CH
Assertion pjds3i 
|- ( ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) /\ ( F C_ ( _|_ ` H ) /\ G C_ ( _|_ ` H ) ) ) -> A = ( ( ( ( projh ` F ) ` A ) +h ( ( projh ` G ) ` A ) ) +h ( ( projh ` H ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 pjds3.1 
 |-  F e. CH
2 pjds3.2 
 |-  G e. CH
3 pjds3.3 
 |-  H e. CH
4 simpl 
 |-  ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) -> A e. ( ( F vH G ) vH H ) )
5 3 choccli 
 |-  ( _|_ ` H ) e. CH
6 1 2 5 chlubii 
 |-  ( ( F C_ ( _|_ ` H ) /\ G C_ ( _|_ ` H ) ) -> ( F vH G ) C_ ( _|_ ` H ) )
7 1 2 chjcli 
 |-  ( F vH G ) e. CH
8 7 3 pjdsi 
 |-  ( ( A e. ( ( F vH G ) vH H ) /\ ( F vH G ) C_ ( _|_ ` H ) ) -> A = ( ( ( projh ` ( F vH G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) )
9 4 6 8 syl2an 
 |-  ( ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) /\ ( F C_ ( _|_ ` H ) /\ G C_ ( _|_ ` H ) ) ) -> A = ( ( ( projh ` ( F vH G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) )
10 1 2 osumi 
 |-  ( F C_ ( _|_ ` G ) -> ( F +H G ) = ( F vH G ) )
11 10 fveq2d 
 |-  ( F C_ ( _|_ ` G ) -> ( projh ` ( F +H G ) ) = ( projh ` ( F vH G ) ) )
12 11 fveq1d 
 |-  ( F C_ ( _|_ ` G ) -> ( ( projh ` ( F +H G ) ) ` A ) = ( ( projh ` ( F vH G ) ) ` A ) )
13 12 oveq1d 
 |-  ( F C_ ( _|_ ` G ) -> ( ( ( projh ` ( F +H G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = ( ( ( projh ` ( F vH G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) )
14 13 ad2antlr 
 |-  ( ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) /\ ( F C_ ( _|_ ` H ) /\ G C_ ( _|_ ` H ) ) ) -> ( ( ( projh ` ( F +H G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = ( ( ( projh ` ( F vH G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) )
15 7 3 chjcli 
 |-  ( ( F vH G ) vH H ) e. CH
16 15 cheli 
 |-  ( A e. ( ( F vH G ) vH H ) -> A e. ~H )
17 1 2 pjsumi 
 |-  ( A e. ~H -> ( F C_ ( _|_ ` G ) -> ( ( projh ` ( F +H G ) ) ` A ) = ( ( ( projh ` F ) ` A ) +h ( ( projh ` G ) ` A ) ) ) )
18 17 imp 
 |-  ( ( A e. ~H /\ F C_ ( _|_ ` G ) ) -> ( ( projh ` ( F +H G ) ) ` A ) = ( ( ( projh ` F ) ` A ) +h ( ( projh ` G ) ` A ) ) )
19 16 18 sylan 
 |-  ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) -> ( ( projh ` ( F +H G ) ) ` A ) = ( ( ( projh ` F ) ` A ) +h ( ( projh ` G ) ` A ) ) )
20 19 oveq1d 
 |-  ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) -> ( ( ( projh ` ( F +H G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = ( ( ( ( projh ` F ) ` A ) +h ( ( projh ` G ) ` A ) ) +h ( ( projh ` H ) ` A ) ) )
21 20 adantr 
 |-  ( ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) /\ ( F C_ ( _|_ ` H ) /\ G C_ ( _|_ ` H ) ) ) -> ( ( ( projh ` ( F +H G ) ) ` A ) +h ( ( projh ` H ) ` A ) ) = ( ( ( ( projh ` F ) ` A ) +h ( ( projh ` G ) ` A ) ) +h ( ( projh ` H ) ` A ) ) )
22 9 14 21 3eqtr2d 
 |-  ( ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) /\ ( F C_ ( _|_ ` H ) /\ G C_ ( _|_ ` H ) ) ) -> A = ( ( ( ( projh ` F ) ` A ) +h ( ( projh ` G ) ` A ) ) +h ( ( projh ` H ) ` A ) ) )