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}}_{\mathscr{H}}$$
Assertion	pjoci	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\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}}_{\mathscr{H}}$$
2	1	pjtoi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
3		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right):\mathscr{H}⟶\mathscr{H}$$
5	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
6	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	6	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
8	4 5 7	hodsi	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
9	2 8	mpbir	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)$$