# Metamath Proof Explorer

## Theorem h1dei

Description: Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis h1deot.1 ${⊢}{B}\in ℋ$
Assertion h1dei ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\left({A}\in ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$

### Proof

Step Hyp Ref Expression
1 h1deot.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 chssii ${⊢}\perp \left(\left\{{B}\right\}\right)\subseteq ℋ$
6 ocel ${⊢}\perp \left(\left\{{B}\right\}\right)\subseteq ℋ\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\left({A}\in ℋ\wedge \forall {x}\in \perp \left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$
7 5 6 ax-mp ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\left({A}\in ℋ\wedge \forall {x}\in \perp \left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0\right)$
8 1 h1deoi ${⊢}{x}\in \perp \left(\left\{{B}\right\}\right)↔\left({x}\in ℋ\wedge {x}{\cdot }_{\mathrm{ih}}{B}=0\right)$
9 orthcom ${⊢}\left({x}\in ℋ\wedge {B}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{B}=0↔{B}{\cdot }_{\mathrm{ih}}{x}=0\right)$
10 1 9 mpan2 ${⊢}{x}\in ℋ\to \left({x}{\cdot }_{\mathrm{ih}}{B}=0↔{B}{\cdot }_{\mathrm{ih}}{x}=0\right)$
11 10 pm5.32i ${⊢}\left({x}\in ℋ\wedge {x}{\cdot }_{\mathrm{ih}}{B}=0\right)↔\left({x}\in ℋ\wedge {B}{\cdot }_{\mathrm{ih}}{x}=0\right)$
12 8 11 bitri ${⊢}{x}\in \perp \left(\left\{{B}\right\}\right)↔\left({x}\in ℋ\wedge {B}{\cdot }_{\mathrm{ih}}{x}=0\right)$
13 12 imbi1i ${⊢}\left({x}\in \perp \left(\left\{{B}\right\}\right)\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)↔\left(\left({x}\in ℋ\wedge {B}{\cdot }_{\mathrm{ih}}{x}=0\right)\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)$
14 impexp ${⊢}\left(\left({x}\in ℋ\wedge {B}{\cdot }_{\mathrm{ih}}{x}=0\right)\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)↔\left({x}\in ℋ\to \left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$
15 13 14 bitri ${⊢}\left({x}\in \perp \left(\left\{{B}\right\}\right)\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)↔\left({x}\in ℋ\to \left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$
16 15 ralbii2 ${⊢}\forall {x}\in \perp \left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)$
17 16 anbi2i ${⊢}\left({A}\in ℋ\wedge \forall {x}\in \perp \left(\left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0\right)↔\left({A}\in ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$
18 7 17 bitri ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\left({A}\in ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$