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

Metamath Proof Explorer

Theorem ocval

Description: Value of orthogonal complement of a subset of Hilbert space. (Contributed by NM, 7-Aug-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion ocval 
|- ( H C_ ~H -> ( _|_ ` H ) = { x e. ~H | A. y e. H ( x .ih y ) = 0 } )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 1 elpw2 
 |-  ( H e. ~P ~H <-> H C_ ~H )
3 raleq 
 |-  ( z = H -> ( A. y e. z ( x .ih y ) = 0 <-> A. y e. H ( x .ih y ) = 0 ) )
4 3 rabbidv 
 |-  ( z = H -> { x e. ~H | A. y e. z ( x .ih y ) = 0 } = { x e. ~H | A. y e. H ( x .ih y ) = 0 } )
5 df-oc 
 |-  _|_ = ( z e. ~P ~H |-> { x e. ~H | A. y e. z ( x .ih y ) = 0 } )
6 1 rabex 
 |-  { x e. ~H | A. y e. H ( x .ih y ) = 0 } e. _V
7 4 5 6 fvmpt 
 |-  ( H e. ~P ~H -> ( _|_ ` H ) = { x e. ~H | A. y e. H ( x .ih y ) = 0 } )
8 2 7 sylbir 
 |-  ( H C_ ~H -> ( _|_ ` H ) = { x e. ~H | A. y e. H ( x .ih y ) = 0 } )