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∈Cℋ
pjidm.2 ⊢A∈ℋ
pjadj.3 ⊢B∈ℋ
Assertion pjaddii ⊢projℎ⁡H⁡A+ℎB=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢H∈Cℋ
2 pjidm.2 ⊢A∈ℋ
3 pjadj.3 ⊢B∈ℋ
4 1 2 pjpji ⊢A=projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A
5 1 3 pjpji ⊢B=projℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡B
6 4 5 oveq12i ⊢A+ℎB=projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A+ℎprojℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡B
7 1 2 pjhclii ⊢projℎ⁡H⁡A∈ℋ
8 1 choccli ⊢⊥⁡H∈Cℋ
9 8 2 pjhclii ⊢projℎ⁡⊥⁡H⁡A∈ℋ
10 1 3 pjhclii ⊢projℎ⁡H⁡B∈ℋ
11 8 3 pjhclii ⊢projℎ⁡⊥⁡H⁡B∈ℋ
12 7 9 10 11 hvadd4i ⊢projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A+ℎprojℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡B=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B
13 6 12 eqtri ⊢A+ℎB=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B
14 13 fveq2i ⊢projℎ⁡H⁡A+ℎB=projℎ⁡H⁡projℎ⁡H⁡A+ℎprojℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B
15 1 chshii ⊢H∈Sℋ
16 1 2 pjclii ⊢projℎ⁡H⁡A∈H
17 1 3 pjclii ⊢projℎ⁡H⁡B∈H
18 shaddcl ⊢H∈Sℋ∧projℎ⁡H⁡A∈H∧projℎ⁡H⁡B∈H→projℎ⁡H⁡A+ℎprojℎ⁡H⁡B∈H
19 15 16 17 18 mp3an ⊢projℎ⁡H⁡A+ℎprojℎ⁡H⁡B∈H
20 8 chshii ⊢⊥⁡H∈Sℋ
21 8 2 pjclii ⊢projℎ⁡⊥⁡H⁡A∈⊥⁡H
22 8 3 pjclii ⊢projℎ⁡⊥⁡H⁡B∈⊥⁡H
23 shaddcl ⊢⊥⁡H∈Sℋ∧projℎ⁡⊥⁡H⁡A∈⊥⁡H∧projℎ⁡⊥⁡H⁡B∈⊥⁡H→projℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B∈⊥⁡H
24 20 21 22 23 mp3an ⊢projℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B∈⊥⁡H
25 1 pjcompi ⊢projℎ⁡H⁡A+ℎprojℎ⁡H⁡B∈H∧projℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B∈⊥⁡H→projℎ⁡H⁡projℎ⁡H⁡A+ℎprojℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B
26 19 24 25 mp2an ⊢projℎ⁡H⁡projℎ⁡H⁡A+ℎprojℎ⁡H⁡B+ℎprojℎ⁡⊥⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡B=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B
27 14 26 eqtri ⊢projℎ⁡H⁡A+ℎB=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B