Theorem pjocvec

Description: The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of Halmos p. 45. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjocvec	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(H\right)=\left\{x\in \mathscr{H}|{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		choccl	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
2		chss	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(H\right)\subseteq \mathscr{H}$$
3	1 2	syl	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(H\right)\subseteq \mathscr{H}$$
4		sseqin2	$$⊢\perp \left(H\right)\subseteq \mathscr{H}\leftrightarrow \mathscr{H}\cap \perp \left(H\right)=\perp \left(H\right)$$
5	3 4	sylib	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \mathscr{H}\cap \perp \left(H\right)=\perp \left(H\right)$$
6		pjoc2	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in \mathscr{H}\right)\to \left(x\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right)$$
7	6	rabbi2dva	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \mathscr{H}\cap \perp \left(H\right)=\left\{x\in \mathscr{H}|{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right\}$$
8	5 7	eqtr3d	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(H\right)=\left\{x\in \mathscr{H}|{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right\}$$