# Metamath Proof Explorer

## Theorem pjorthcoi

Description: Composition of projections of orthogonal subspaces. Part (i)->(iia) of Theorem 27.4 of Halmos p. 45. (Contributed by NM, 6-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjorthcoi ${⊢}{G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={0}_{\mathrm{hop}}$

### Proof

Step Hyp Ref Expression
1 pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 2 pjcli ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in {H}$
4 1 2 chsscon2i ${⊢}{G}\subseteq \perp \left({H}\right)↔{H}\subseteq \perp \left({G}\right)$
5 ssel ${⊢}{H}\subseteq \perp \left({G}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in \perp \left({G}\right)\right)$
6 4 5 sylbi ${⊢}{G}\subseteq \perp \left({H}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in \perp \left({G}\right)\right)$
7 3 6 syl5com ${⊢}{x}\in ℋ\to \left({G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in \perp \left({G}\right)\right)$
8 2 pjhcli ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in ℋ$
9 pjoc2 ${⊢}\left({G}\in {\mathbf{C}}_{ℋ}\wedge {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in \perp \left({G}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={0}_{ℎ}\right)$
10 1 8 9 sylancr ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in \perp \left({G}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={0}_{ℎ}\right)$
11 7 10 sylibd ${⊢}{x}\in ℋ\to \left({G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={0}_{ℎ}\right)$
12 11 impcom ${⊢}\left({G}\subseteq \perp \left({H}\right)\wedge {x}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={0}_{ℎ}$
13 1 2 pjcoi ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)$
14 13 adantl ${⊢}\left({G}\subseteq \perp \left({H}\right)\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)$
15 ho0val ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
16 15 adantl ${⊢}\left({G}\subseteq \perp \left({H}\right)\wedge {x}\in ℋ\right)\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
17 12 14 16 3eqtr4d ${⊢}\left({G}\subseteq \perp \left({H}\right)\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
18 17 ralrimiva ${⊢}{G}\subseteq \perp \left({H}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
19 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
20 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
21 19 20 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right):ℋ⟶ℋ$
22 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
23 21 22 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={0}_{\mathrm{hop}}$
24 18 23 sylib ${⊢}{G}\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={0}_{\mathrm{hop}}$