# Metamath Proof Explorer

## Theorem pjscji

Description: The projection of orthogonal subspaces 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 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)$

### Proof

Step Hyp Ref Expression
1 pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 pjcjt2 ${⊢}\left({G}\in {\mathbf{C}}_{ℋ}\wedge {H}\in {\mathbf{C}}_{ℋ}\wedge {x}\in ℋ\right)\to \left({G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)$
4 1 2 3 mp3an12 ${⊢}{x}\in ℋ\to \left({G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)$
5 4 impcom ${⊢}\left({G}\subseteq \perp \left({H}\right)\wedge {x}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)$
6 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
7 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
8 hosval ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ\wedge {\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)$
9 6 7 8 mp3an12 ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)$
10 9 adantl ${⊢}\left({G}\subseteq \perp \left({H}\right)\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)$
11 5 10 eqtr4d ${⊢}\left({G}\subseteq \perp \left({H}\right)\wedge {x}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)\left({x}\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)$
12 11 ralrimiva ${⊢}{G}\subseteq \perp \left({H}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)\left({x}\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)$
13 1 2 chjcli ${⊢}{G}{\vee }_{ℋ}{H}\in {\mathbf{C}}_{ℋ}$
14 13 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right):ℋ⟶ℋ$
15 6 7 hoaddcli ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right):ℋ⟶ℋ$
16 14 15 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)\left({x}\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)↔{\mathrm{proj}}_{ℎ}\left({G}{\vee }_{ℋ}{H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)$
17 12 16 sylib ${⊢}{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)$