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