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

Metamath Proof Explorer

Theorem h1de2ci

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 21-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis h1de2ct.1 
|- B e. ~H
Assertion h1de2ci 
|- ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC A = ( x .h B ) )

Proof

Step Hyp Ref Expression
1 h1de2ct.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 choccli 
 |-  ( _|_ ` ( _|_ ` { B } ) ) e. CH
6 5 cheli 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> A e. ~H )
7 hvmulcl 
 |-  ( ( x e. CC /\ B e. ~H ) -> ( x .h B ) e. ~H )
8 1 7 mpan2 
 |-  ( x e. CC -> ( x .h B ) e. ~H )
9 eleq1 
 |-  ( A = ( x .h B ) -> ( A e. ~H <-> ( x .h B ) e. ~H ) )
10 8 9 syl5ibrcom 
 |-  ( x e. CC -> ( A = ( x .h B ) -> A e. ~H ) )
11 10 rexlimiv 
 |-  ( E. x e. CC A = ( x .h B ) -> A e. ~H )
12 eleq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) ) )
13 eqeq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A = ( x .h B ) <-> if ( A e. ~H , A , 0h ) = ( x .h B ) ) )
14 13 rexbidv 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( E. x e. CC A = ( x .h B ) <-> E. x e. CC if ( A e. ~H , A , 0h ) = ( x .h B ) ) )
15 12 14 bibi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC A = ( x .h B ) ) <-> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC if ( A e. ~H , A , 0h ) = ( x .h B ) ) ) )
16 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
17 16 1 h1de2ctlem 
 |-  ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC if ( A e. ~H , A , 0h ) = ( x .h B ) )
18 15 17 dedth 
 |-  ( A e. ~H -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC A = ( x .h B ) ) )
19 6 11 18 pm5.21nii 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC A = ( x .h B ) )