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