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 ∈ ℋ
Assertion h1de2ci ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B

Proof

Step Hyp Ref Expression
1 h1de2ct.1 ⊢ B ∈ ℋ
2 snssi ⊢ B ∈ ℋ → B ⊆ ℋ
3 occl ⊢ B ⊆ ℋ → ⊥ ⁡ B ∈ C ℋ
4 1 2 3 mp2b ⊢ ⊥ ⁡ B ∈ C ℋ
5 4 choccli ⊢ ⊥ ⁡ ⊥ ⁡ B ∈ C ℋ
6 5 cheli ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → A ∈ ℋ
7 hvmulcl ⊢ x ∈ ℂ ∧ B ∈ ℋ → x ⋅ ℎ B ∈ ℋ
8 1 7 mpan2 ⊢ x ∈ ℂ → x ⋅ ℎ B ∈ ℋ
9 eleq1 ⊢ A = x ⋅ ℎ B → A ∈ ℋ ↔ x ⋅ ℎ B ∈ ℋ
10 8 9 syl5ibrcom ⊢ x ∈ ℂ → A = x ⋅ ℎ B → A ∈ ℋ
11 10 rexlimiv ⊢ ∃ x ∈ ℂ A = x ⋅ ℎ B → A ∈ ℋ
12 eleq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ if A ∈ ℋ A 0 ℎ ∈ ⊥ ⁡ ⊥ ⁡ B
13 eqeq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A = x ⋅ ℎ B ↔ if A ∈ ℋ A 0 ℎ = x ⋅ ℎ B
14 13 rexbidv ⊢ A = if A ∈ ℋ A 0 ℎ → ∃ x ∈ ℂ A = x ⋅ ℎ B ↔ ∃ x ∈ ℂ if A ∈ ℋ A 0 ℎ = x ⋅ ℎ B
15 12 14 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B ↔ if A ∈ ℋ A 0 ℎ ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ if A ∈ ℋ A 0 ℎ = x ⋅ ℎ B
16 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
17 16 1 h1de2ctlem ⊢ if A ∈ ℋ A 0 ℎ ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ if A ∈ ℋ A 0 ℎ = x ⋅ ℎ B
18 15 17 dedth ⊢ A ∈ ℋ → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B
19 6 11 18 pm5.21nii ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B