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