# 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 ) ) )`
` |-  ( ( ( ( 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 ) ) )`