Metamath Proof Explorer

Theorem pjsubii

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

Ref Expression
Hypotheses pjidm.1 ⊢H∈Cℋ
pjidm.2 ⊢A∈ℋ
pjsub.3 ⊢B∈ℋ
Assertion pjsubii ⊢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 pjsub.3 ⊢B∈ℋ
4 neg1cn ⊢−1∈ℂ
5 4 3 hvmulcli ⊢-1⋅ℎB∈ℋ
6 1 2 5 pjaddii ⊢projℎ⁡H⁡A+ℎ-1⋅ℎB=projℎ⁡H⁡A+ℎprojℎ⁡H⁡-1⋅ℎB
7 1 3 4 pjmulii ⊢projℎ⁡H⁡-1⋅ℎB=-1⋅ℎprojℎ⁡H⁡B
8 7 oveq2i ⊢projℎ⁡H⁡A+ℎprojℎ⁡H⁡-1⋅ℎB=projℎ⁡H⁡A+ℎ-1⋅ℎprojℎ⁡H⁡B
9 6 8 eqtri ⊢projℎ⁡H⁡A+ℎ-1⋅ℎB=projℎ⁡H⁡A+ℎ-1⋅ℎprojℎ⁡H⁡B
10 2 3 hvsubvali ⊢A-ℎB=A+ℎ-1⋅ℎB
11 10 fveq2i ⊢projℎ⁡H⁡A-ℎB=projℎ⁡H⁡A+ℎ-1⋅ℎB
12 1 2 pjhclii ⊢projℎ⁡H⁡A∈ℋ
13 1 3 pjhclii ⊢projℎ⁡H⁡B∈ℋ
14 12 13 hvsubvali ⊢projℎ⁡H⁡A-ℎprojℎ⁡H⁡B=projℎ⁡H⁡A+ℎ-1⋅ℎprojℎ⁡H⁡B
15 9 11 14 3eqtr4i ⊢projℎ⁡H⁡A-ℎB=projℎ⁡H⁡A-ℎprojℎ⁡H⁡B