Theorem h1deoi

Description: Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Hypothesis	h1deot.1	|- B e. ~H
Assertion	h1deoi	|- ( A e. ( _|_ ` { B } ) <-> ( A e. ~H /\ ( A .ih B ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		h1deot.1	|- B e. ~H
2		snssi	|- ( B e. ~H -> { B } C_ ~H )
3		ocel	|- ( { B } C_ ~H -> ( A e. ( _|_ ` { B } ) <-> ( A e. ~H /\ A. x e. { B } ( A .ih x ) = 0 ) ) )
4	1 2 3	mp2b	|- ( A e. ( _|_ ` { B } ) <-> ( A e. ~H /\ A. x e. { B } ( A .ih x ) = 0 ) )
5	1	elexi	|- B e. _V
6		oveq2	|- ( x = B -> ( A .ih x ) = ( A .ih B ) )
7	6	eqeq1d	|- ( x = B -> ( ( A .ih x ) = 0 <-> ( A .ih B ) = 0 ) )
8	5 7	ralsn	|- ( A. x e. { B } ( A .ih x ) = 0 <-> ( A .ih B ) = 0 )
9	8	anbi2i	|- ( ( A e. ~H /\ A. x e. { B } ( A .ih x ) = 0 ) <-> ( A e. ~H /\ ( A .ih B ) = 0 ) )
10	4 9	bitri	|- ( A e. ( _|_ ` { B } ) <-> ( A e. ~H /\ ( A .ih B ) = 0 ) )