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	⊢ 𝐵 ∈ ℋ
Assertion	h1de2ci	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		h1de2ct.1	⊢ 𝐵 ∈ ℋ
2		snssi	⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
3		occl	⊢ ( { 𝐵 } ⊆ ℋ → ( ⊥ ‘ { 𝐵 } ) ∈ Cℋ )
4	1 2 3	mp2b	⊢ ( ⊥ ‘ { 𝐵 } ) ∈ Cℋ
5	4	choccli	⊢ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∈ Cℋ
6	5	cheli	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → 𝐴 ∈ ℋ )
7		hvmulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ·ℎ 𝐵 ) ∈ ℋ )
8	1 7	mpan2	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ·ℎ 𝐵 ) ∈ ℋ )
9		eleq1	⊢ ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( 𝐴 ∈ ℋ ↔ ( 𝑥 ·ℎ 𝐵 ) ∈ ℋ ) )
10	8 9	syl5ibrcom	⊢ ( 𝑥 ∈ ℂ → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → 𝐴 ∈ ℋ ) )
11	10	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → 𝐴 ∈ ℋ )
12		eleq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
13		eqeq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) ) )
14	13	rexbidv	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ↔ ∃ 𝑥 ∈ ℂ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) ) )
15	12 14	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) ) ) )
16		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
17	16 1	h1de2ctlem	⊢ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) = ( 𝑥 ·ℎ 𝐵 ) )
18	15 17	dedth	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) )
19	6 11 18	pm5.21nii	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) )