# Metamath Proof Explorer

## Theorem pjoci

Description: Projection of orthocomplement. First part of Theorem 27.3 of Halmos p. 45. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis pjidmco.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjoci ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)$

### Proof

Step Hyp Ref Expression
1 pjidmco.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 1 pjtoi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)={\mathrm{proj}}_{ℎ}\left(ℋ\right)$
3 helch ${⊢}ℋ\in {\mathbf{C}}_{ℋ}$
4 3 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right):ℋ⟶ℋ$
5 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
6 1 choccli ${⊢}\perp \left({H}\right)\in {\mathbf{C}}_{ℋ}$
7 6 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right):ℋ⟶ℋ$
8 4 5 7 hodsi ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)↔{\mathrm{proj}}_{ℎ}\left({H}\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)={\mathrm{proj}}_{ℎ}\left(ℋ\right)$
9 2 8 mpbir ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)$