Metamath Proof Explorer


Theorem ocel

Description: Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ocel
|- ( H C_ ~H -> ( A e. ( _|_ ` H ) <-> ( A e. ~H /\ A. x e. H ( A .ih x ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 ocval
 |-  ( H C_ ~H -> ( _|_ ` H ) = { y e. ~H | A. x e. H ( y .ih x ) = 0 } )
2 1 eleq2d
 |-  ( H C_ ~H -> ( A e. ( _|_ ` H ) <-> A e. { y e. ~H | A. x e. H ( y .ih x ) = 0 } ) )
3 oveq1
 |-  ( y = A -> ( y .ih x ) = ( A .ih x ) )
4 3 eqeq1d
 |-  ( y = A -> ( ( y .ih x ) = 0 <-> ( A .ih x ) = 0 ) )
5 4 ralbidv
 |-  ( y = A -> ( A. x e. H ( y .ih x ) = 0 <-> A. x e. H ( A .ih x ) = 0 ) )
6 5 elrab
 |-  ( A e. { y e. ~H | A. x e. H ( y .ih x ) = 0 } <-> ( A e. ~H /\ A. x e. H ( A .ih x ) = 0 ) )
7 2 6 syl6bb
 |-  ( H C_ ~H -> ( A e. ( _|_ ` H ) <-> ( A e. ~H /\ A. x e. H ( A .ih x ) = 0 ) ) )