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=ifA∈ℋA0ℎ→A∈⊥⁡⊥⁡B↔ifA∈ℋA0ℎ∈⊥⁡⊥⁡B
13 eqeq1 ⊢A=ifA∈ℋA0ℎ→A=x⋅ℎB↔ifA∈ℋA0ℎ=x⋅ℎB
14 13 rexbidv ⊢A=ifA∈ℋA0ℎ→∃x∈ℂA=x⋅ℎB↔∃x∈ℂifA∈ℋA0ℎ=x⋅ℎB
15 12 14 bibi12d ⊢A=ifA∈ℋA0ℎ→A∈⊥⁡⊥⁡B↔∃x∈ℂA=x⋅ℎB↔ifA∈ℋA0ℎ∈⊥⁡⊥⁡B↔∃x∈ℂifA∈ℋA0ℎ=x⋅ℎB
16 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
17 16 1 h1de2ctlem ⊢ifA∈ℋA0ℎ∈⊥⁡⊥⁡B↔∃x∈ℂifA∈ℋA0ℎ=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