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

Metamath Proof Explorer

Theorem h1dei

Description: Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 h1deot.1 
 |-  B e. ~H
2 snssi 
 |-  ( B e. ~H -> { B } C_ ~H )
3 occl 
 |-  ( { B } C_ ~H -> ( _|_ ` { B } ) e. CH )
4 1 2 3 mp2b 
 |-  ( _|_ ` { B } ) e. CH
5 4 chssii 
 |-  ( _|_ ` { B } ) C_ ~H
6 ocel 
 |-  ( ( _|_ ` { B } ) C_ ~H -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) ) )
7 5 6 ax-mp 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) )
8 1 h1deoi 
 |-  ( x e. ( _|_ ` { B } ) <-> ( x e. ~H /\ ( x .ih B ) = 0 ) )
9 orthcom 
 |-  ( ( x e. ~H /\ B e. ~H ) -> ( ( x .ih B ) = 0 <-> ( B .ih x ) = 0 ) )
10 1 9 mpan2 
 |-  ( x e. ~H -> ( ( x .ih B ) = 0 <-> ( B .ih x ) = 0 ) )
11 10 pm5.32i 
 |-  ( ( x e. ~H /\ ( x .ih B ) = 0 ) <-> ( x e. ~H /\ ( B .ih x ) = 0 ) )
12 8 11 bitri 
 |-  ( x e. ( _|_ ` { B } ) <-> ( x e. ~H /\ ( B .ih x ) = 0 ) )
13 12 imbi1i 
 |-  ( ( x e. ( _|_ ` { B } ) -> ( A .ih x ) = 0 ) <-> ( ( x e. ~H /\ ( B .ih x ) = 0 ) -> ( A .ih x ) = 0 ) )
14 impexp 
 |-  ( ( ( x e. ~H /\ ( B .ih x ) = 0 ) -> ( A .ih x ) = 0 ) <-> ( x e. ~H -> ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )
15 13 14 bitri 
 |-  ( ( x e. ( _|_ ` { B } ) -> ( A .ih x ) = 0 ) <-> ( x e. ~H -> ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )
16 15 ralbii2 
 |-  ( A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 <-> A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) )
17 16 anbi2i 
 |-  ( ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )
18 7 17 bitri 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )