Theorem pjoccoi

Description: Composition of projections of a subspace and its orthocomplement. (Contributed by NM, 14-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjidmco.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjoccoi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		pjidmco.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	chssii	$$⊢H\subseteq \mathscr{H}$$
3		ococss	$$⊢H\subseteq \mathscr{H}\to H\subseteq \perp \left(\perp \left(H\right)\right)$$
4	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	1 4	pjorthcoi	$$⊢H\subseteq \perp \left(\perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)=0_{\mathrm{hop}}$$
6	2 3 5	mp2b	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)=0_{\mathrm{hop}}$$