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 = LHyp K
dvh3dim.u U = DVecH K W
dvh3dim.v V = Base U
dvh3dim.n N = LSpan U
dvh3dim.k φ K HL W H
dvh3dim.x φ X V
dvh3dim.y φ Y V
dvh3dim2.z φ Z V
Assertion dvh4dimN φ z V ¬ z N X Y Z

Proof

Step Hyp Ref Expression
1 dvh3dim.h H = LHyp K
2 dvh3dim.u U = DVecH K W
3 dvh3dim.v V = Base U
4 dvh3dim.n N = LSpan U
5 dvh3dim.k φ K HL W H
6 dvh3dim.x φ X V
7 dvh3dim.y φ Y V
8 dvh3dim2.z φ Z V
9 1 2 3 4 5 7 8 dvh3dim φ z V ¬ z N Y Z
10 9 adantr φ X = 0 U z V ¬ z N Y Z
11 eqid 0 U = 0 U
12 1 2 5 dvhlmod φ U LMod
13 prssi Y V Z V Y Z V
14 7 8 13 syl2anc φ Y Z V
15 3 11 4 12 14 lspun0 φ N Y Z 0 U = N Y Z
16 tprot 0 U Y Z = Y Z 0 U
17 df-tp Y Z 0 U = Y Z 0 U
18 16 17 eqtr2i Y Z 0 U = 0 U Y Z
19 tpeq1 X = 0 U X Y Z = 0 U Y Z
20 18 19 eqtr4id X = 0 U Y Z 0 U = X Y Z
21 20 fveq2d X = 0 U N Y Z 0 U = N X Y Z
22 15 21 sylan9req φ X = 0 U N Y Z = N X Y Z
23 22 eleq2d φ X = 0 U z N Y Z z N X Y Z
24 23 notbid φ X = 0 U ¬ z N Y Z ¬ z N X Y Z
25 24 rexbidv φ X = 0 U z V ¬ z N Y Z z V ¬ z N X Y Z
26 10 25 mpbid φ X = 0 U z V ¬ z N X Y Z
27 1 2 3 4 5 6 8 dvh3dim φ z V ¬ z N X Z
28 27 adantr φ Y = 0 U z V ¬ z N X Z
29 prssi X V Z V X Z V
30 6 8 29 syl2anc φ X Z V
31 3 11 4 12 30 lspun0 φ N X Z 0 U = N X Z
32 df-tp X Z 0 U = X Z 0 U
33 tpcomb X Z 0 U = X 0 U Z
34 32 33 eqtr3i X Z 0 U = X 0 U Z
35 tpeq2 Y = 0 U X Y Z = X 0 U Z
36 34 35 eqtr4id Y = 0 U X Z 0 U = X Y Z
37 36 fveq2d Y = 0 U N X Z 0 U = N X Y Z
38 31 37 sylan9req φ Y = 0 U N X Z = N X Y Z
39 38 eleq2d φ Y = 0 U z N X Z z N X Y Z
40 39 notbid φ Y = 0 U ¬ z N X Z ¬ z N X Y Z
41 40 rexbidv φ Y = 0 U z V ¬ z N X Z z V ¬ z N X Y Z
42 28 41 mpbid φ Y = 0 U z V ¬ z N X Y Z
43 1 2 3 4 5 6 7 dvh3dim φ z V ¬ z N X Y
44 43 adantr φ Z = 0 U z V ¬ z N X Y
45 prssi X V Y V X Y V
46 6 7 45 syl2anc φ X Y V
47 3 11 4 12 46 lspun0 φ N X Y 0 U = N X Y
48 tpeq3 Z = 0 U X Y Z = X Y 0 U
49 df-tp X Y 0 U = X Y 0 U
50 48 49 eqtr2di Z = 0 U X Y 0 U = X Y Z
51 50 fveq2d Z = 0 U N X Y 0 U = N X Y Z
52 47 51 sylan9req φ Z = 0 U N X Y = N X Y Z
53 52 eleq2d φ Z = 0 U z N X Y z N X Y Z
54 53 notbid φ Z = 0 U ¬ z N X Y ¬ z N X Y Z
55 54 rexbidv φ Z = 0 U z V ¬ z N X Y z V ¬ z N X Y Z
56 44 55 mpbid φ Z = 0 U z V ¬ z N X Y Z
57 5 adantr φ X 0 U Y 0 U Z 0 U K HL W H
58 6 adantr φ X 0 U Y 0 U Z 0 U X V
59 7 adantr φ X 0 U Y 0 U Z 0 U Y V
60 8 adantr φ X 0 U Y 0 U Z 0 U Z V
61 simpr1 φ X 0 U Y 0 U Z 0 U X 0 U
62 simpr2 φ X 0 U Y 0 U Z 0 U Y 0 U
63 simpr3 φ X 0 U Y 0 U Z 0 U Z 0 U
64 1 2 3 4 57 58 59 60 11 61 62 63 dvh4dimlem φ X 0 U Y 0 U Z 0 U z V ¬ z N X Y Z
65 26 42 56 64 pm2.61da3ne φ z V ¬ z N X Y Z