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 HCH=x|projHx=0

Proof

Step Hyp Ref Expression
1 choccl HCHC
2 chss HCH
3 1 2 syl HCH
4 sseqin2 HH=H
5 3 4 sylib HCH=H
6 pjoc2 HCxxHprojHx=0
7 6 rabbi2dva HCH=x|projHx=0
8 5 7 eqtr3d HCH=x|projHx=0