Metamath Proof Explorer

Theorem pjaddii

Description: Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 
|- H e. CH
pjidm.2 
|- A e. ~H
pjadj.3 
|- B e. ~H
Assertion pjaddii 
|- ( ( projh ` H ) ` ( A +h B ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 
 |-  H e. CH
2 pjidm.2 
 |-  A e. ~H
3 pjadj.3 
 |-  B e. ~H
4 1 2 pjpji 
 |-  A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )
5 1 3 pjpji 
 |-  B = ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) )
6 4 5 oveq12i 
 |-  ( A +h B ) = ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) +h ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) )
7 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
8 1 choccli 
 |-  ( _|_ ` H ) e. CH
9 8 2 pjhclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H
10 1 3 pjhclii 
 |-  ( ( projh ` H ) ` B ) e. ~H
11 8 3 pjhclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` B ) e. ~H
12 7 9 10 11 hvadd4i 
 |-  ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) +h ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) +h ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) )
13 6 12 eqtri 
 |-  ( A +h B ) = ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) +h ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) )
14 13 fveq2i 
 |-  ( ( projh ` H ) ` ( A +h B ) ) = ( ( projh ` H ) ` ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) +h ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) )
15 1 chshii 
 |-  H e. SH
16 1 2 pjclii 
 |-  ( ( projh ` H ) ` A ) e. H
17 1 3 pjclii 
 |-  ( ( projh ` H ) ` B ) e. H
18 shaddcl 
 |-  ( ( H e. SH /\ ( ( projh ` H ) ` A ) e. H /\ ( ( projh ` H ) ` B ) e. H ) -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) e. H )
19 15 16 17 18 mp3an 
 |-  ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) e. H
20 8 chshii 
 |-  ( _|_ ` H ) e. SH
21 8 2 pjclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H )
22 8 3 pjclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` B ) e. ( _|_ ` H )
23 shaddcl 
 |-  ( ( ( _|_ ` H ) e. SH /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) /\ ( ( projh ` ( _|_ ` H ) ) ` B ) e. ( _|_ ` H ) ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) e. ( _|_ ` H ) )
24 20 21 22 23 mp3an 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) e. ( _|_ ` H )
25 1 pjcompi 
 |-  ( ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) e. H /\ ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) e. ( _|_ ` H ) ) -> ( ( projh ` H ) ` ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) +h ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) )
26 19 24 25 mp2an 
 |-  ( ( projh ` H ) ` ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) ) +h ( ( ( projh ` ( _|_ ` H ) ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) )
27 14 26 eqtri 
 |-  ( ( projh ` H ) ` ( A +h B ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` B ) )