# Metamath Proof Explorer

## Theorem h1de2bi

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 19-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h1de2.1 ${⊢}{A}\in ℋ$
h1de2.2 ${⊢}{B}\in ℋ$
Assertion h1de2bi ${⊢}{B}\ne {0}_{ℎ}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔{A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\right)$

### Proof

Step Hyp Ref Expression
1 h1de2.1 ${⊢}{A}\in ℋ$
2 h1de2.2 ${⊢}{B}\in ℋ$
3 his6 ${⊢}{B}\in ℋ\to \left({B}{\cdot }_{\mathrm{ih}}{B}=0↔{B}={0}_{ℎ}\right)$
4 2 3 ax-mp ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}=0↔{B}={0}_{ℎ}$
5 4 necon3bii ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0↔{B}\ne {0}_{ℎ}$
6 1 2 h1de2i ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to \left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}$
7 6 adantl ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{B}\ne 0\wedge {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to \left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}$
8 7 oveq2d ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{B}\ne 0\wedge {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)=\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)$
9 2 2 hicli ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
10 9 recclzi ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ$
11 ax-hvmulass ${⊢}\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\wedge {B}{\cdot }_{\mathrm{ih}}{B}\in ℂ\wedge {A}\in ℋ\right)\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)$
12 9 1 11 mp3an23 ${⊢}\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)$
13 10 12 syl ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)$
14 ax-1cn ${⊢}1\in ℂ$
15 14 9 divcan1zi ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right)=1$
16 15 oveq1d ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=1{\cdot }_{ℎ}{A}$
17 13 16 eqtr3d ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)=1{\cdot }_{ℎ}{A}$
18 ax-hvmulid ${⊢}{A}\in ℋ\to 1{\cdot }_{ℎ}{A}={A}$
19 1 18 ax-mp ${⊢}1{\cdot }_{ℎ}{A}={A}$
20 17 19 syl6eq ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)={A}$
21 20 adantr ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{B}\ne 0\wedge {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)={A}$
22 8 21 eqtr3d ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{B}\ne 0\wedge {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)={A}$
23 1 2 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
24 ax-hvmulass ${⊢}\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{B}\in ℂ\wedge {B}\in ℋ\right)\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}=\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)$
25 23 2 24 mp3an23 ${⊢}\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}=\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)$
26 10 25 syl ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}=\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)$
27 mulcom ${⊢}\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{B}\in ℂ\right)\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right)=\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)$
28 10 23 27 sylancl ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right)=\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)$
29 23 9 divreczi ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}=\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)$
30 28 29 eqtr4d ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right)=\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}$
31 30 oveq1d ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}$
32 26 31 eqtr3d ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}$
33 32 adantr ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{B}\ne 0\wedge {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to \left(\frac{1}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}$
34 22 33 eqtr3d ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{B}\ne 0\wedge {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to {A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}$
35 34 ex ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to {A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\right)$
36 23 9 divclzi ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ$
37 2 elexi ${⊢}{B}\in \mathrm{V}$
38 37 snss ${⊢}{B}\in ℋ↔\left\{{B}\right\}\subseteq ℋ$
39 2 38 mpbi ${⊢}\left\{{B}\right\}\subseteq ℋ$
40 occl ${⊢}\left\{{B}\right\}\subseteq ℋ\to \perp \left(\left\{{B}\right\}\right)\in {\mathbf{C}}_{ℋ}$
41 39 40 ax-mp ${⊢}\perp \left(\left\{{B}\right\}\right)\in {\mathbf{C}}_{ℋ}$
42 41 choccli ${⊢}\perp \left(\perp \left(\left\{{B}\right\}\right)\right)\in {\mathbf{C}}_{ℋ}$
43 42 chshii ${⊢}\perp \left(\perp \left(\left\{{B}\right\}\right)\right)\in {\mathbf{S}}_{ℋ}$
44 h1did ${⊢}{B}\in ℋ\to {B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
45 2 44 ax-mp ${⊢}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
46 shmulcl ${⊢}\left(\perp \left(\perp \left(\left\{{B}\right\}\right)\right)\in {\mathbf{S}}_{ℋ}\wedge \frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\wedge {B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to \left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
47 43 45 46 mp3an13 ${⊢}\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\to \left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
48 36 47 syl ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
49 eleq1 ${⊢}{A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)$
50 48 49 syl5ibrcom ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left({A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\to {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)$
51 35 50 impbid ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔{A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\right)$
52 5 51 sylbir ${⊢}{B}\ne {0}_{ℎ}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔{A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\right)$