Theorem pjvec

Description: The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

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

Proof

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