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