This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. CH -> ( _|_ ` H ) = { x e. ~H | ( ( projh ` H ) ` x ) = 0h } )

Proof

Step Hyp Ref Expression
1 choccl 
 |-  ( H e. CH -> ( _|_ ` H ) e. CH )
2 chss 
 |-  ( ( _|_ ` H ) e. CH -> ( _|_ ` H ) C_ ~H )
3 1 2 syl 
 |-  ( H e. CH -> ( _|_ ` H ) C_ ~H )
4 sseqin2 
 |-  ( ( _|_ ` H ) C_ ~H <-> ( ~H i^i ( _|_ ` H ) ) = ( _|_ ` H ) )
5 3 4 sylib 
 |-  ( H e. CH -> ( ~H i^i ( _|_ ` H ) ) = ( _|_ ` H ) )
6 pjoc2 
 |-  ( ( H e. CH /\ x e. ~H ) -> ( x e. ( _|_ ` H ) <-> ( ( projh ` H ) ` x ) = 0h ) )
7 6 rabbi2dva 
 |-  ( H e. CH -> ( ~H i^i ( _|_ ` H ) ) = { x e. ~H | ( ( projh ` H ) ` x ) = 0h } )
8 5 7 eqtr3d 
 |-  ( H e. CH -> ( _|_ ` H ) = { x e. ~H | ( ( projh ` H ) ` x ) = 0h } )