# 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}\in ℋ$
Assertion h1de2ci ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$

### Proof

Step Hyp Ref Expression
1 h1de2ct.1 ${⊢}{B}\in ℋ$
2 snssi ${⊢}{B}\in ℋ\to \left\{{B}\right\}\subseteq ℋ$
3 occl ${⊢}\left\{{B}\right\}\subseteq ℋ\to \perp \left(\left\{{B}\right\}\right)\in {\mathbf{C}}_{ℋ}$
4 1 2 3 mp2b ${⊢}\perp \left(\left\{{B}\right\}\right)\in {\mathbf{C}}_{ℋ}$
5 4 choccli ${⊢}\perp \left(\perp \left(\left\{{B}\right\}\right)\right)\in {\mathbf{C}}_{ℋ}$
6 5 cheli ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to {A}\in ℋ$
7 hvmulcl ${⊢}\left({x}\in ℂ\wedge {B}\in ℋ\right)\to {x}{\cdot }_{ℎ}{B}\in ℋ$
8 1 7 mpan2 ${⊢}{x}\in ℂ\to {x}{\cdot }_{ℎ}{B}\in ℋ$
9 eleq1 ${⊢}{A}={x}{\cdot }_{ℎ}{B}\to \left({A}\in ℋ↔{x}{\cdot }_{ℎ}{B}\in ℋ\right)$
10 8 9 syl5ibrcom ${⊢}{x}\in ℂ\to \left({A}={x}{\cdot }_{ℎ}{B}\to {A}\in ℋ\right)$
11 10 rexlimiv ${⊢}\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}\to {A}\in ℋ$
12 eleq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)$
13 eqeq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({A}={x}{\cdot }_{ℎ}{B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={x}{\cdot }_{ℎ}{B}\right)$
14 13 rexbidv ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={x}{\cdot }_{ℎ}{B}\right)$
15 12 14 bibi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={x}{\cdot }_{ℎ}{B}\right)\right)$
16 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
17 16 1 h1de2ctlem ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={x}{\cdot }_{ℎ}{B}$
18 15 17 dedth ${⊢}{A}\in ℋ\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}\right)$
19 6 11 18 pm5.21nii ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$