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 C
pjidm.2 A
pjmul.3 C
Assertion pjmulii proj H C A = C proj H A

Proof

Step Hyp Ref Expression
1 pjidm.1 H C
2 pjidm.2 A
3 pjmul.3 C
4 1 2 pjpji A = proj H A + proj H A
5 4 oveq2i C A = C proj H A + proj H A
6 1 2 pjhclii proj H A
7 1 choccli H C
8 7 2 pjhclii proj H A
9 3 6 8 hvdistr1i C proj H A + proj H A = C proj H A + C proj H A
10 5 9 eqtri C A = C proj H A + C proj H A
11 10 fveq2i proj H C A = proj H C proj H A + C proj H A
12 1 chshii H S
13 1 2 pjclii proj H A H
14 shmulcl H S C proj H A H C proj H A H
15 12 3 13 14 mp3an C proj H A H
16 7 chshii H S
17 7 2 pjclii proj H A H
18 shmulcl H S C proj H A H C proj H A H
19 16 3 17 18 mp3an C proj H A H
20 1 pjcompi C proj H A H C proj H A H proj H C proj H A + C proj H A = C proj H A
21 15 19 20 mp2an proj H C proj H A + C proj H A = C proj H A
22 11 21 eqtri proj H C A = C proj H A