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 } )