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

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 bitrdi 
 |-  ( H C_ ~H -> ( A e. ( _|_ ` H ) <-> ( A e. ~H /\ A. x e. H ( A .ih x ) = 0 ) ) )