# Metamath Proof Explorer

## Theorem dvh4dimN

Description: There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015) (New usage is discouraged.)

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}$
dvh3dim2.z ${⊢}{\phi }\to {Z}\in {V}$
Assertion dvh4dimN ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\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 dvh3dim2.z ${⊢}{\phi }\to {Z}\in {V}$
9 1 2 3 4 5 7 8 dvh3dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
10 9 adantr ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
11 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
12 1 2 5 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
13 prssi ${⊢}\left({Y}\in {V}\wedge {Z}\in {V}\right)\to \left\{{Y},{Z}\right\}\subseteq {V}$
14 7 8 13 syl2anc ${⊢}{\phi }\to \left\{{Y},{Z}\right\}\subseteq {V}$
15 3 11 4 12 14 lspun0 ${⊢}{\phi }\to {N}\left(\left\{{Y},{Z}\right\}\cup \left\{{0}_{{U}}\right\}\right)={N}\left(\left\{{Y},{Z}\right\}\right)$
16 tprot ${⊢}\left\{{0}_{{U}},{Y},{Z}\right\}=\left\{{Y},{Z},{0}_{{U}}\right\}$
17 df-tp ${⊢}\left\{{Y},{Z},{0}_{{U}}\right\}=\left\{{Y},{Z}\right\}\cup \left\{{0}_{{U}}\right\}$
18 16 17 eqtr2i ${⊢}\left\{{Y},{Z}\right\}\cup \left\{{0}_{{U}}\right\}=\left\{{0}_{{U}},{Y},{Z}\right\}$
19 tpeq1 ${⊢}{X}={0}_{{U}}\to \left\{{X},{Y},{Z}\right\}=\left\{{0}_{{U}},{Y},{Z}\right\}$
20 18 19 eqtr4id ${⊢}{X}={0}_{{U}}\to \left\{{Y},{Z}\right\}\cup \left\{{0}_{{U}}\right\}=\left\{{X},{Y},{Z}\right\}$
21 20 fveq2d ${⊢}{X}={0}_{{U}}\to {N}\left(\left\{{Y},{Z}\right\}\cup \left\{{0}_{{U}}\right\}\right)={N}\left(\left\{{X},{Y},{Z}\right\}\right)$
22 15 21 sylan9req ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to {N}\left(\left\{{Y},{Z}\right\}\right)={N}\left(\left\{{X},{Y},{Z}\right\}\right)$
23 22 eleq2d ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left({z}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
24 23 notbid ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left(¬{z}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
25 24 rexbidv ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \left(\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
26 10 25 mpbid ${⊢}\left({\phi }\wedge {X}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)$
27 1 2 3 4 5 6 8 dvh3dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Z}\right\}\right)$
28 27 adantr ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Z}\right\}\right)$
29 prssi ${⊢}\left({X}\in {V}\wedge {Z}\in {V}\right)\to \left\{{X},{Z}\right\}\subseteq {V}$
30 6 8 29 syl2anc ${⊢}{\phi }\to \left\{{X},{Z}\right\}\subseteq {V}$
31 3 11 4 12 30 lspun0 ${⊢}{\phi }\to {N}\left(\left\{{X},{Z}\right\}\cup \left\{{0}_{{U}}\right\}\right)={N}\left(\left\{{X},{Z}\right\}\right)$
32 df-tp ${⊢}\left\{{X},{Z},{0}_{{U}}\right\}=\left\{{X},{Z}\right\}\cup \left\{{0}_{{U}}\right\}$
33 tpcomb ${⊢}\left\{{X},{Z},{0}_{{U}}\right\}=\left\{{X},{0}_{{U}},{Z}\right\}$
34 32 33 eqtr3i ${⊢}\left\{{X},{Z}\right\}\cup \left\{{0}_{{U}}\right\}=\left\{{X},{0}_{{U}},{Z}\right\}$
35 tpeq2 ${⊢}{Y}={0}_{{U}}\to \left\{{X},{Y},{Z}\right\}=\left\{{X},{0}_{{U}},{Z}\right\}$
36 34 35 eqtr4id ${⊢}{Y}={0}_{{U}}\to \left\{{X},{Z}\right\}\cup \left\{{0}_{{U}}\right\}=\left\{{X},{Y},{Z}\right\}$
37 36 fveq2d ${⊢}{Y}={0}_{{U}}\to {N}\left(\left\{{X},{Z}\right\}\cup \left\{{0}_{{U}}\right\}\right)={N}\left(\left\{{X},{Y},{Z}\right\}\right)$
38 31 37 sylan9req ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Z}\right\}\right)={N}\left(\left\{{X},{Y},{Z}\right\}\right)$
39 38 eleq2d ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \left({z}\in {N}\left(\left\{{X},{Z}\right\}\right)↔{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
40 39 notbid ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \left(¬{z}\in {N}\left(\left\{{X},{Z}\right\}\right)↔¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
41 40 rexbidv ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \left(\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Z}\right\}\right)↔\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
42 28 41 mpbid ${⊢}\left({\phi }\wedge {Y}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)$
43 1 2 3 4 5 6 7 dvh3dim ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$
44 43 adantr ${⊢}\left({\phi }\wedge {Z}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$
45 prssi ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left\{{X},{Y}\right\}\subseteq {V}$
46 6 7 45 syl2anc ${⊢}{\phi }\to \left\{{X},{Y}\right\}\subseteq {V}$
47 3 11 4 12 46 lspun0 ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\cup \left\{{0}_{{U}}\right\}\right)={N}\left(\left\{{X},{Y}\right\}\right)$
48 tpeq3 ${⊢}{Z}={0}_{{U}}\to \left\{{X},{Y},{Z}\right\}=\left\{{X},{Y},{0}_{{U}}\right\}$
49 df-tp ${⊢}\left\{{X},{Y},{0}_{{U}}\right\}=\left\{{X},{Y}\right\}\cup \left\{{0}_{{U}}\right\}$
50 48 49 eqtr2di ${⊢}{Z}={0}_{{U}}\to \left\{{X},{Y}\right\}\cup \left\{{0}_{{U}}\right\}=\left\{{X},{Y},{Z}\right\}$
51 50 fveq2d ${⊢}{Z}={0}_{{U}}\to {N}\left(\left\{{X},{Y}\right\}\cup \left\{{0}_{{U}}\right\}\right)={N}\left(\left\{{X},{Y},{Z}\right\}\right)$
52 47 51 sylan9req ${⊢}\left({\phi }\wedge {Z}={0}_{{U}}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X},{Y},{Z}\right\}\right)$
53 52 eleq2d ${⊢}\left({\phi }\wedge {Z}={0}_{{U}}\right)\to \left({z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
54 53 notbid ${⊢}\left({\phi }\wedge {Z}={0}_{{U}}\right)\to \left(¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)↔¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)\right)$
55 54 rexbidv ${⊢}\left({\phi }\wedge {Z}={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},{Y},{Z}\right\}\right)\right)$
56 44 55 mpbid ${⊢}\left({\phi }\wedge {Z}={0}_{{U}}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)$
57 5 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
58 6 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to {X}\in {V}$
59 7 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to {Y}\in {V}$
60 8 adantr ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to {Z}\in {V}$
61 simpr1 ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to {X}\ne {0}_{{U}}$
62 simpr2 ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to {Y}\ne {0}_{{U}}$
63 simpr3 ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to {Z}\ne {0}_{{U}}$
64 1 2 3 4 57 58 59 60 11 61 62 63 dvh4dimlem ${⊢}\left({\phi }\wedge \left({X}\ne {0}_{{U}}\wedge {Y}\ne {0}_{{U}}\wedge {Z}\ne {0}_{{U}}\right)\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)$
65 26 42 56 64 pm2.61da3ne ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Z}\right\}\right)$