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

Metamath Proof Explorer

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