# Metamath Proof Explorer

## Theorem dvh2dim

Description: There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015)

Ref Expression
Hypotheses dvh3dim.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvh3dim.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvh3dim.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dvh3dim.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
dvh3dim.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dvh3dim.x ${⊢}{\phi }\to {X}\in {V}$
Assertion dvh2dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 dvh3dim.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dvh3dim.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dvh3dim.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 dvh3dim.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
5 dvh3dim.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 dvh3dim.x ${⊢}{\phi }\to {X}\in {V}$
7 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
8 1 2 3 7 5 dvh1dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}{z}\ne {0}_{{U}}$
9 8 adantr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}{z}\ne {0}_{{U}}$
10 simpr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {X}={0}_{{U}}$
11 10 sneqd ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left\{{X}\right\}=\left\{{0}_{{U}}\right\}$
12 11 fveq2d ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{0}_{{U}}\right\}\right)$
13 1 2 5 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
14 7 4 lspsn0 ${⊢}{U}\in \mathrm{LMod}\to {N}\left(\left\{{0}_{{U}}\right\}\right)=\left\{{0}_{{U}}\right\}$
15 13 14 syl ${⊢}{\phi }\to {N}\left(\left\{{0}_{{U}}\right\}\right)=\left\{{0}_{{U}}\right\}$
16 15 adantr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{0}_{{U}}\right\}\right)=\left\{{0}_{{U}}\right\}$
17 12 16 eqtrd ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X}\right\}\right)=\left\{{0}_{{U}}\right\}$
18 17 eleq2d ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left({z}\in {N}\left(\left\{{X}\right\}\right)↔{z}\in \left\{{0}_{{U}}\right\}\right)$
19 velsn ${⊢}{z}\in \left\{{0}_{{U}}\right\}↔{z}={0}_{{U}}$
20 18 19 syl6bb ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left({z}\in {N}\left(\left\{{X}\right\}\right)↔{z}={0}_{{U}}\right)$
21 20 necon3bbid ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left(¬{z}\in {N}\left(\left\{{X}\right\}\right)↔{z}\ne {0}_{{U}}\right)$
22 21 rexbidv ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left(\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)↔\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}{z}\ne {0}_{{U}}\right)$
23 9 22 mpbird ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)$
24 5 adantr ${⊢}\left({\phi }\wedge {X}\ne {0}_{{U}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
25 6 adantr ${⊢}\left({\phi }\wedge {X}\ne {0}_{{U}}\right)\to {X}\in {V}$
26 simpr ${⊢}\left({\phi }\wedge {X}\ne {0}_{{U}}\right)\to {X}\ne {0}_{{U}}$
27 1 2 3 4 24 25 25 7 26 26 dvhdimlem ${⊢}\left({\phi }\wedge {X}\ne {0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{X}\right\}\right)$
28 dfsn2 ${⊢}\left\{{X}\right\}=\left\{{X},{X}\right\}$
29 28 fveq2i ${⊢}{N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{X},{X}\right\}\right)$
30 29 eleq2i ${⊢}{z}\in {N}\left(\left\{{X}\right\}\right)↔{z}\in {N}\left(\left\{{X},{X}\right\}\right)$
31 30 notbii ${⊢}¬{z}\in {N}\left(\left\{{X}\right\}\right)↔¬{z}\in {N}\left(\left\{{X},{X}\right\}\right)$
32 31 rexbii ${⊢}\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)↔\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{X}\right\}\right)$
33 27 32 sylibr ${⊢}\left({\phi }\wedge {X}\ne {0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)$
34 23 33 pm2.61dane ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)$