Metamath Proof Explorer

Theorem pjmulii

Description: Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 
|- H e. CH
pjidm.2 
|- A e. ~H
pjmul.3 
|- C e. CC
Assertion pjmulii 
|- ( ( projh ` H ) ` ( C .h A ) ) = ( C .h ( ( projh ` H ) ` A ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 
 |-  H e. CH
2 pjidm.2 
 |-  A e. ~H
3 pjmul.3 
 |-  C e. CC
4 1 2 pjpji 
 |-  A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )
5 4 oveq2i 
 |-  ( C .h A ) = ( C .h ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
6 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
7 1 choccli 
 |-  ( _|_ ` H ) e. CH
8 7 2 pjhclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H
9 3 6 8 hvdistr1i 
 |-  ( C .h ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) = ( ( C .h ( ( projh ` H ) ` A ) ) +h ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
10 5 9 eqtri 
 |-  ( C .h A ) = ( ( C .h ( ( projh ` H ) ` A ) ) +h ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
11 10 fveq2i 
 |-  ( ( projh ` H ) ` ( C .h A ) ) = ( ( projh ` H ) ` ( ( C .h ( ( projh ` H ) ` A ) ) +h ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) )
12 1 chshii 
 |-  H e. SH
13 1 2 pjclii 
 |-  ( ( projh ` H ) ` A ) e. H
14 shmulcl 
 |-  ( ( H e. SH /\ C e. CC /\ ( ( projh ` H ) ` A ) e. H ) -> ( C .h ( ( projh ` H ) ` A ) ) e. H )
15 12 3 13 14 mp3an 
 |-  ( C .h ( ( projh ` H ) ` A ) ) e. H
16 7 chshii 
 |-  ( _|_ ` H ) e. SH
17 7 2 pjclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H )
18 shmulcl 
 |-  ( ( ( _|_ ` H ) e. SH /\ C e. CC /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) ) -> ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) e. ( _|_ ` H ) )
19 16 3 17 18 mp3an 
 |-  ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) e. ( _|_ ` H )
20 1 pjcompi 
 |-  ( ( ( C .h ( ( projh ` H ) ` A ) ) e. H /\ ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) e. ( _|_ ` H ) ) -> ( ( projh ` H ) ` ( ( C .h ( ( projh ` H ) ` A ) ) +h ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) ) = ( C .h ( ( projh ` H ) ` A ) ) )
21 15 19 20 mp2an 
 |-  ( ( projh ` H ) ` ( ( C .h ( ( projh ` H ) ` A ) ) +h ( C .h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) ) = ( C .h ( ( projh ` H ) ` A ) )
22 11 21 eqtri 
 |-  ( ( projh ` H ) ` ( C .h A ) ) = ( C .h ( ( projh ` H ) ` A ) )