Metamath Proof Explorer

Theorem pjsumi

Description: The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjsumt.1 ⊢G∈Cℋ
pjsumt.2 ⊢H∈Cℋ
Assertion pjsumi ⊢A∈ℋ→G⊆⊥⁡H→projℎ⁡G+ℋH⁡A=projℎ⁡G⁡A+ℎprojℎ⁡H⁡A

Proof

Step Hyp Ref Expression
1 pjsumt.1 ⊢G∈Cℋ
2 pjsumt.2 ⊢H∈Cℋ
3 1 2 osumi ⊢G⊆⊥⁡H→G+ℋH=G∨ℋH
4 3 fveq2d ⊢G⊆⊥⁡H→projℎ⁡G+ℋH=projℎ⁡G∨ℋH
5 4 fveq1d ⊢G⊆⊥⁡H→projℎ⁡G+ℋH⁡A=projℎ⁡G∨ℋH⁡A
6 5 adantl ⊢A∈ℋ∧G⊆⊥⁡H→projℎ⁡G+ℋH⁡A=projℎ⁡G∨ℋH⁡A
7 pjcjt2 ⊢G∈Cℋ∧H∈Cℋ∧A∈ℋ→G⊆⊥⁡H→projℎ⁡G∨ℋH⁡A=projℎ⁡G⁡A+ℎprojℎ⁡H⁡A
8 1 2 7 mp3an12 ⊢A∈ℋ→G⊆⊥⁡H→projℎ⁡G∨ℋH⁡A=projℎ⁡G⁡A+ℎprojℎ⁡H⁡A
9 8 imp ⊢A∈ℋ∧G⊆⊥⁡H→projℎ⁡G∨ℋH⁡A=projℎ⁡G⁡A+ℎprojℎ⁡H⁡A
10 6 9 eqtrd ⊢A∈ℋ∧G⊆⊥⁡H→projℎ⁡G+ℋH⁡A=projℎ⁡G⁡A+ℎprojℎ⁡H⁡A
11 10 ex ⊢A∈ℋ→G⊆⊥⁡H→projℎ⁡G+ℋH⁡A=projℎ⁡G⁡A+ℎprojℎ⁡H⁡A