Metamath Proof Explorer

Theorem pjcji

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

Ref Expression
Hypotheses pjidm.1 ⊢H∈Cℋ
pjidm.2 ⊢A∈ℋ
pjsslem.1 ⊢G∈Cℋ
Assertion pjcji ⊢H⊆⊥⁡G→projℎ⁡H∨ℋG⁡A=projℎ⁡H⁡A+ℎprojℎ⁡G⁡A

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢H∈Cℋ
2 pjidm.2 ⊢A∈ℋ
3 pjsslem.1 ⊢G∈Cℋ
4 3 choccli ⊢⊥⁡G∈Cℋ
5 1 2 4 pjssmii ⊢H⊆⊥⁡G→projℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A=projℎ⁡⊥⁡G∩⊥⁡H⁡A
6 5 oveq2d ⊢H⊆⊥⁡G→A-ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A=A-ℎprojℎ⁡⊥⁡G∩⊥⁡H⁡A
7 3 2 pjpoi ⊢projℎ⁡G⁡A=A-ℎprojℎ⁡⊥⁡G⁡A
8 7 oveq2i ⊢projℎ⁡H⁡A+ℎprojℎ⁡G⁡A=projℎ⁡H⁡A+ℎA-ℎprojℎ⁡⊥⁡G⁡A
9 4 2 pjhclii ⊢projℎ⁡⊥⁡G⁡A∈ℋ
10 1 2 pjhclii ⊢projℎ⁡H⁡A∈ℋ
11 9 10 hvnegdii ⊢-1⋅ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A=projℎ⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A
12 11 oveq2i ⊢A+ℎ-1⋅ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A=A+ℎprojℎ⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A
13 hvaddsub12 ⊢projℎ⁡H⁡A∈ℋ∧A∈ℋ∧projℎ⁡⊥⁡G⁡A∈ℋ→projℎ⁡H⁡A+ℎA-ℎprojℎ⁡⊥⁡G⁡A=A+ℎprojℎ⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A
14 10 2 9 13 mp3an ⊢projℎ⁡H⁡A+ℎA-ℎprojℎ⁡⊥⁡G⁡A=A+ℎprojℎ⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A
15 12 14 eqtr4i ⊢A+ℎ-1⋅ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A=projℎ⁡H⁡A+ℎA-ℎprojℎ⁡⊥⁡G⁡A
16 8 15 eqtr4i ⊢projℎ⁡H⁡A+ℎprojℎ⁡G⁡A=A+ℎ-1⋅ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A
17 9 10 hvsubcli ⊢projℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A∈ℋ
18 2 17 hvsubvali ⊢A-ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A=A+ℎ-1⋅ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A
19 16 18 eqtr4i ⊢projℎ⁡H⁡A+ℎprojℎ⁡G⁡A=A-ℎprojℎ⁡⊥⁡G⁡A-ℎprojℎ⁡H⁡A
20 1 3 chjcomi ⊢H∨ℋG=G∨ℋH
21 3 1 chdmm4i ⊢⊥⁡⊥⁡G∩⊥⁡H=G∨ℋH
22 20 21 eqtr4i ⊢H∨ℋG=⊥⁡⊥⁡G∩⊥⁡H
23 22 fveq2i ⊢projℎ⁡H∨ℋG=projℎ⁡⊥⁡⊥⁡G∩⊥⁡H
24 23 fveq1i ⊢projℎ⁡H∨ℋG⁡A=projℎ⁡⊥⁡⊥⁡G∩⊥⁡H⁡A
25 1 choccli ⊢⊥⁡H∈Cℋ
26 4 25 chincli ⊢⊥⁡G∩⊥⁡H∈Cℋ
27 26 2 pjopi ⊢projℎ⁡⊥⁡⊥⁡G∩⊥⁡H⁡A=A-ℎprojℎ⁡⊥⁡G∩⊥⁡H⁡A
28 24 27 eqtri ⊢projℎ⁡H∨ℋG⁡A=A-ℎprojℎ⁡⊥⁡G∩⊥⁡H⁡A
29 6 19 28 3eqtr4g ⊢H⊆⊥⁡G→projℎ⁡H⁡A+ℎprojℎ⁡G⁡A=projℎ⁡H∨ℋG⁡A
30 29 eqcomd ⊢H⊆⊥⁡G→projℎ⁡H∨ℋG⁡A=projℎ⁡H⁡A+ℎprojℎ⁡G⁡A