# Metamath Proof Explorer

## 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}}_{ℋ}\to \perp \left({H}\right)=\left\{{x}\in ℋ|{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)={0}_{ℎ}\right\}$

### Proof

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