Metamath Proof Explorer

Theorem pjcji

Description: The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 
|- H e. CH
pjidm.2 
|- A e. ~H
pjsslem.1 
|- G e. CH
Assertion pjcji 
|- ( H C_ ( _|_ ` G ) -> ( ( projh ` ( H vH G ) ) ` A ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 
 |-  H e. CH
2 pjidm.2 
 |-  A e. ~H
3 pjsslem.1 
 |-  G e. CH
4 3 choccli 
 |-  ( _|_ ` G ) e. CH
5 1 2 4 pjssmii 
 |-  ( H C_ ( _|_ ` G ) -> ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ` A ) )
6 5 oveq2d 
 |-  ( H C_ ( _|_ ` G ) -> ( A -h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( A -h ( ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ` A ) ) )
7 3 2 pjpoi 
 |-  ( ( projh ` G ) ` A ) = ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) )
8 7 oveq2i 
 |-  ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( ( ( projh ` H ) ` A ) +h ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) )
9 4 2 pjhclii 
 |-  ( ( projh ` ( _|_ ` G ) ) ` A ) e. ~H
10 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
11 9 10 hvnegdii 
 |-  ( -u 1 .h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( ( ( projh ` H ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) )
12 11 oveq2i 
 |-  ( A +h ( -u 1 .h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) ) ) = ( A +h ( ( ( projh ` H ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) )
13 hvaddsub12 
 |-  ( ( ( ( projh ` H ) ` A ) e. ~H /\ A e. ~H /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ~H ) -> ( ( ( projh ` H ) ` A ) +h ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) ) = ( A +h ( ( ( projh ` H ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) ) )
14 10 2 9 13 mp3an 
 |-  ( ( ( projh ` H ) ` A ) +h ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) ) = ( A +h ( ( ( projh ` H ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) )
15 12 14 eqtr4i 
 |-  ( A +h ( -u 1 .h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) ) ) = ( ( ( projh ` H ) ` A ) +h ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) )
16 8 15 eqtr4i 
 |-  ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( A +h ( -u 1 .h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) ) )
17 9 10 hvsubcli 
 |-  ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ~H
18 2 17 hvsubvali 
 |-  ( A -h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( A +h ( -u 1 .h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) ) )
19 16 18 eqtr4i 
 |-  ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( A -h ( ( ( projh ` ( _|_ ` G ) ) ` A ) -h ( ( projh ` H ) ` A ) ) )
20 1 3 chjcomi 
 |-  ( H vH G ) = ( G vH H )
21 3 1 chdmm4i 
 |-  ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) = ( G vH H )
22 20 21 eqtr4i 
 |-  ( H vH G ) = ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) )
23 22 fveq2i 
 |-  ( projh ` ( H vH G ) ) = ( projh ` ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) )
24 23 fveq1i 
 |-  ( ( projh ` ( H vH G ) ) ` A ) = ( ( projh ` ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ` A )
25 1 choccli 
 |-  ( _|_ ` H ) e. CH
26 4 25 chincli 
 |-  ( ( _|_ ` G ) i^i ( _|_ ` H ) ) e. CH
27 26 2 pjopi 
 |-  ( ( projh ` ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ` A ) = ( A -h ( ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ` A ) )
28 24 27 eqtri 
 |-  ( ( projh ` ( H vH G ) ) ` A ) = ( A -h ( ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ` A ) )
29 6 19 28 3eqtr4g 
 |-  ( H C_ ( _|_ ` G ) -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( ( projh ` ( H vH G ) ) ` A ) )
30 29 eqcomd 
 |-  ( H C_ ( _|_ ` G ) -> ( ( projh ` ( H vH G ) ) ` A ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) )