# 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}\in {\mathbf{C}}_{ℋ}$
pjidm.2 ${⊢}{A}\in ℋ$
pjsslem.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
Assertion pjcji ${⊢}{H}\subseteq \perp \left({G}\right)\to {\mathrm{proj}}_{ℎ}\left({H}{\vee }_{ℋ}{G}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 pjidm.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 pjidm.2 ${⊢}{A}\in ℋ$
3 pjsslem.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
4 3 choccli ${⊢}\perp \left({G}\right)\in {\mathbf{C}}_{ℋ}$
5 1 2 4 pjssmii ${⊢}{H}\subseteq \perp \left({G}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)\left({A}\right)$
6 5 oveq2d ${⊢}{H}\subseteq \perp \left({G}\right)\to {A}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)\left({A}\right)$
7 3 2 pjpoi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)={A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)$
8 7 oveq2i ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}\left({A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\right)$
9 4 2 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in ℋ$
10 1 2 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ$
11 9 10 hvnegdii ${⊢}-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)$
12 11 oveq2i ${⊢}{A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)={A}{+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\right)$
13 hvaddsub12 ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ\wedge {A}\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}\left({A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\right)={A}{+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\right)$
14 10 2 9 13 mp3an ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}\left({A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\right)={A}{+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\right)$
15 12 14 eqtr4i ${⊢}{A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}\left({A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\right)$
16 8 15 eqtr4i ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)$
17 9 10 hvsubcli ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ$
18 2 17 hvsubvali ${⊢}{A}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)$
19 16 18 eqtr4i ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)={A}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)$
20 1 3 chjcomi ${⊢}{H}{\vee }_{ℋ}{G}={G}{\vee }_{ℋ}{H}$
21 3 1 chdmm4i ${⊢}\perp \left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)={G}{\vee }_{ℋ}{H}$
22 20 21 eqtr4i ${⊢}{H}{\vee }_{ℋ}{G}=\perp \left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)$
23 22 fveq2i ${⊢}{\mathrm{proj}}_{ℎ}\left({H}{\vee }_{ℋ}{G}\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)\right)$
24 23 fveq1i ${⊢}{\mathrm{proj}}_{ℎ}\left({H}{\vee }_{ℋ}{G}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)\right)\left({A}\right)$
25 1 choccli ${⊢}\perp \left({H}\right)\in {\mathbf{C}}_{ℋ}$
26 4 25 chincli ${⊢}\perp \left({G}\right)\cap \perp \left({H}\right)\in {\mathbf{C}}_{ℋ}$
27 26 2 pjopi ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)\right)\left({A}\right)={A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)\left({A}\right)$
28 24 27 eqtri ${⊢}{\mathrm{proj}}_{ℎ}\left({H}{\vee }_{ℋ}{G}\right)\left({A}\right)={A}{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\cap \perp \left({H}\right)\right)\left({A}\right)$
29 6 19 28 3eqtr4g ${⊢}{H}\subseteq \perp \left({G}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}{\vee }_{ℋ}{G}\right)\left({A}\right)$
30 29 eqcomd ${⊢}{H}\subseteq \perp \left({G}\right)\to {\mathrm{proj}}_{ℎ}\left({H}{\vee }_{ℋ}{G}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)$