# Metamath Proof Explorer

## Theorem pjssumi

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

### Proof

Step Hyp Ref Expression
1 pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 1 2 osumi ${⊢}{G}\subseteq \perp \left({H}\right)\to {G}{+}_{ℋ}{H}={G}{\vee }_{ℋ}{H}$
4 3 fveq2d ${⊢}{G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}{+}_{ℋ}{H}\right)={\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)$
5 1 2 pjscji ${⊢}{G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)$
6 4 5 eqtrd ${⊢}{G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}{+}_{ℋ}{H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)$