# Metamath Proof Explorer

## Theorem dvh3dim

Description: There is a vector that is outside the span of 2 others. (Contributed by NM, 24-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}$
dvh3dim.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion dvh3dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\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 dvh3dim.y ${⊢}{\phi }\to {Y}\in {V}$
8 1 2 3 4 5 7 dvh2dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{Y}\right\}\right)$
9 8 adantr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{Y}\right\}\right)$
10 prcom ${⊢}\left\{{X},{Y}\right\}=\left\{{Y},{X}\right\}$
11 preq2 ${⊢}{X}={0}_{{U}}\to \left\{{Y},{X}\right\}=\left\{{Y},{0}_{{U}}\right\}$
12 10 11 syl5eq ${⊢}{X}={0}_{{U}}\to \left\{{X},{Y}\right\}=\left\{{Y},{0}_{{U}}\right\}$
13 12 fveq2d ${⊢}{X}={0}_{{U}}\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{Y},{0}_{{U}}\right\}\right)$
14 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
15 1 2 5 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
16 3 14 4 15 7 lsppr0 ${⊢}{\phi }\to {N}\left(\left\{{Y},{0}_{{U}}\right\}\right)={N}\left(\left\{{Y}\right\}\right)$
17 13 16 sylan9eqr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{Y}\right\}\right)$
18 17 eleq2d ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left({z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔{z}\in {N}\left(\left\{{Y}\right\}\right)\right)$
19 18 notbid ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left(¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔¬{z}\in {N}\left(\left\{{Y}\right\}\right)\right)$
20 19 rexbidv ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left(\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{Y}\right\}\right)\right)$
21 9 20 mpbird ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$
22 1 2 3 4 5 6 dvh2dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)$
23 22 adantr ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)$
24 preq2 ${⊢}{Y}={0}_{{U}}\to \left\{{X},{Y}\right\}=\left\{{X},{0}_{{U}}\right\}$
25 24 fveq2d ${⊢}{Y}={0}_{{U}}\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X},{0}_{{U}}\right\}\right)$
26 3 14 4 15 6 lsppr0 ${⊢}{\phi }\to {N}\left(\left\{{X},{0}_{{U}}\right\}\right)={N}\left(\left\{{X}\right\}\right)$
27 25 26 sylan9eqr ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X}\right\}\right)$
28 27 eleq2d ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \left({z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔{z}\in {N}\left(\left\{{X}\right\}\right)\right)$
29 28 notbid ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \left(¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)$
30 29 rexbidv ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \left(\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)$
31 23 30 mpbird ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$
32 5 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
33 6 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {X}\in {V}$
34 7 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {Y}\in {V}$
35 simprl ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {X}\ne {0}_{{U}}$
36 simprr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to {Y}\ne {0}_{{U}}$
37 1 2 3 4 32 33 34 14 35 36 dvhdimlem ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\right)\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$
38 21 31 37 pm2.61da2ne ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$