Metamath Proof Explorer


Theorem dvh3dim3N

Description: There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 everywhere. If this one is needed, make dvh3dim2 into a lemma. (Contributed by NM, 21-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
dvh3dim3.t φ T V
Assertion dvh3dim3N φ z V ¬ z N X Y ¬ z N Z T

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 dvh3dim3.t φ T V
10 eqid LSubSp U = LSubSp U
11 1 2 5 dvhlmod φ U LMod
12 11 adantr φ Y N Z T U LMod
13 3 10 4 11 8 9 lspprcl φ N Z T LSubSp U
14 13 adantr φ Y N Z T N Z T LSubSp U
15 simpr φ Y N Z T Y N Z T
16 3 4 11 8 9 lspprid2 φ T N Z T
17 16 adantr φ Y N Z T T N Z T
18 10 4 12 14 15 17 lspprss φ Y N Z T N Y T N Z T
19 sspss N Y T N Z T N Y T N Z T N Y T = N Z T
20 18 19 sylib φ Y N Z T N Y T N Z T N Y T = N Z T
21 1 2 5 dvhlvec φ U LVec
22 21 adantr φ N Y T N Z T U LVec
23 3 10 4 11 7 9 lspprcl φ N Y T LSubSp U
24 23 adantr φ N Y T N Z T N Y T LSubSp U
25 8 adantr φ N Y T N Z T Z V
26 9 adantr φ N Y T N Z T T V
27 simpr φ N Y T N Z T N Y T N Z T
28 3 10 4 22 24 25 26 27 lspprat φ N Y T N Z T w V N Y T = N w
29 5 3ad2ant1 φ w V N Y T = N w K HL W H
30 simp2 φ w V N Y T = N w w V
31 6 3ad2ant1 φ w V N Y T = N w X V
32 8 3ad2ant1 φ w V N Y T = N w Z V
33 1 2 3 4 29 30 31 32 dvh3dim2 φ w V N Y T = N w z V ¬ z N w X ¬ z N w Z
34 11 3ad2ant1 φ w V N Y T = N w U LMod
35 10 lsssssubg U LMod LSubSp U SubGrp U
36 34 35 syl φ w V N Y T = N w LSubSp U SubGrp U
37 3 10 4 lspsncl U LMod X V N X LSubSp U
38 11 6 37 syl2anc φ N X LSubSp U
39 38 3ad2ant1 φ w V N Y T = N w N X LSubSp U
40 36 39 sseldd φ w V N Y T = N w N X SubGrp U
41 3 10 4 lspsncl U LMod w V N w LSubSp U
42 34 30 41 syl2anc φ w V N Y T = N w N w LSubSp U
43 36 42 sseldd φ w V N Y T = N w N w SubGrp U
44 prssi Y V T V Y T V
45 7 9 44 syl2anc φ Y T V
46 snsspr1 Y Y T
47 46 a1i φ Y Y T
48 3 4 lspss U LMod Y T V Y Y T N Y N Y T
49 11 45 47 48 syl3anc φ N Y N Y T
50 49 3ad2ant1 φ w V N Y T = N w N Y N Y T
51 simp3 φ w V N Y T = N w N Y T = N w
52 50 51 sseqtrd φ w V N Y T = N w N Y N w
53 eqid LSSum U = LSSum U
54 53 lsmless2 N X SubGrp U N w SubGrp U N Y N w N X LSSum U N Y N X LSSum U N w
55 40 43 52 54 syl3anc φ w V N Y T = N w N X LSSum U N Y N X LSSum U N w
56 3 4 53 11 6 7 lsmpr φ N X Y = N X LSSum U N Y
57 56 3ad2ant1 φ w V N Y T = N w N X Y = N X LSSum U N Y
58 prcom w X = X w
59 58 fveq2i N w X = N X w
60 3 4 53 34 31 30 lsmpr φ w V N Y T = N w N X w = N X LSSum U N w
61 59 60 syl5eq φ w V N Y T = N w N w X = N X LSSum U N w
62 55 57 61 3sstr4d φ w V N Y T = N w N X Y N w X
63 62 ssneld φ w V N Y T = N w ¬ z N w X ¬ z N X Y
64 3 10 4 lspsncl U LMod Z V N Z LSubSp U
65 11 8 64 syl2anc φ N Z LSubSp U
66 65 3ad2ant1 φ w V N Y T = N w N Z LSubSp U
67 36 66 sseldd φ w V N Y T = N w N Z SubGrp U
68 snsspr2 T Y T
69 68 a1i φ T Y T
70 3 4 lspss U LMod Y T V T Y T N T N Y T
71 11 45 69 70 syl3anc φ N T N Y T
72 71 3ad2ant1 φ w V N Y T = N w N T N Y T
73 72 51 sseqtrd φ w V N Y T = N w N T N w
74 53 lsmless2 N Z SubGrp U N w SubGrp U N T N w N Z LSSum U N T N Z LSSum U N w
75 67 43 73 74 syl3anc φ w V N Y T = N w N Z LSSum U N T N Z LSSum U N w
76 3 4 53 11 8 9 lsmpr φ N Z T = N Z LSSum U N T
77 76 3ad2ant1 φ w V N Y T = N w N Z T = N Z LSSum U N T
78 prcom w Z = Z w
79 78 fveq2i N w Z = N Z w
80 3 4 53 34 32 30 lsmpr φ w V N Y T = N w N Z w = N Z LSSum U N w
81 79 80 syl5eq φ w V N Y T = N w N w Z = N Z LSSum U N w
82 75 77 81 3sstr4d φ w V N Y T = N w N Z T N w Z
83 82 ssneld φ w V N Y T = N w ¬ z N w Z ¬ z N Z T
84 63 83 anim12d φ w V N Y T = N w ¬ z N w X ¬ z N w Z ¬ z N X Y ¬ z N Z T
85 84 reximdv φ w V N Y T = N w z V ¬ z N w X ¬ z N w Z z V ¬ z N X Y ¬ z N Z T
86 33 85 mpd φ w V N Y T = N w z V ¬ z N X Y ¬ z N Z T
87 86 rexlimdv3a φ w V N Y T = N w z V ¬ z N X Y ¬ z N Z T
88 87 adantr φ N Y T N Z T w V N Y T = N w z V ¬ z N X Y ¬ z N Z T
89 28 88 mpd φ N Y T N Z T z V ¬ z N X Y ¬ z N Z T
90 1 2 3 4 5 7 6 9 dvh3dim2 φ z V ¬ z N Y X ¬ z N Y T
91 90 adantr φ N Y T = N Z T z V ¬ z N Y X ¬ z N Y T
92 simpr φ N Y T = N Z T N Y T = N Z T
93 prcom Y X = X Y
94 93 fveq2i N Y X = N X Y
95 94 eleq2i z N Y X z N X Y
96 95 notbii ¬ z N Y X ¬ z N X Y
97 96 a1i N Y T = N Z T ¬ z N Y X ¬ z N X Y
98 eleq2 N Y T = N Z T z N Y T z N Z T
99 98 notbid N Y T = N Z T ¬ z N Y T ¬ z N Z T
100 97 99 anbi12d N Y T = N Z T ¬ z N Y X ¬ z N Y T ¬ z N X Y ¬ z N Z T
101 92 100 syl φ N Y T = N Z T ¬ z N Y X ¬ z N Y T ¬ z N X Y ¬ z N Z T
102 101 rexbidv φ N Y T = N Z T z V ¬ z N Y X ¬ z N Y T z V ¬ z N X Y ¬ z N Z T
103 91 102 mpbid φ N Y T = N Z T z V ¬ z N X Y ¬ z N Z T
104 89 103 jaodan φ N Y T N Z T N Y T = N Z T z V ¬ z N X Y ¬ z N Z T
105 20 104 syldan φ Y N Z T z V ¬ z N X Y ¬ z N Z T
106 1 2 3 4 5 7 6 9 dvh3dim2 φ w V ¬ w N Y X ¬ w N Y T
107 106 adantr φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T
108 simpl1l φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T φ
109 108 11 syl φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T U LMod
110 simpl2 φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T w V
111 108 7 syl φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T Y V
112 eqid + U = + U
113 3 112 lmodvacl U LMod w V Y V w + U Y V
114 109 110 111 113 syl3anc φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T w + U Y V
115 3 10 4 11 6 7 lspprcl φ N X Y LSubSp U
116 108 115 syl φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T N X Y LSubSp U
117 3 4 11 6 7 lspprid2 φ Y N X Y
118 108 117 syl φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T Y N X Y
119 simpl3l φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T ¬ w N Y X
120 94 eleq2i w N Y X w N X Y
121 119 120 sylnib φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T ¬ w N X Y
122 3 112 10 109 116 118 110 121 lssvancl2 φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T ¬ w + U Y N X Y
123 108 13 syl φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T N Z T LSubSp U
124 simpr φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T w N Z T
125 simpl1r φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T ¬ Y N Z T
126 3 112 10 109 123 124 111 125 lssvancl1 φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T ¬ w + U Y N Z T
127 eleq1 z = w + U Y z N X Y w + U Y N X Y
128 127 notbid z = w + U Y ¬ z N X Y ¬ w + U Y N X Y
129 eleq1 z = w + U Y z N Z T w + U Y N Z T
130 129 notbid z = w + U Y ¬ z N Z T ¬ w + U Y N Z T
131 128 130 anbi12d z = w + U Y ¬ z N X Y ¬ z N Z T ¬ w + U Y N X Y ¬ w + U Y N Z T
132 131 rspcev w + U Y V ¬ w + U Y N X Y ¬ w + U Y N Z T z V ¬ z N X Y ¬ z N Z T
133 114 122 126 132 syl12anc φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T w N Z T z V ¬ z N X Y ¬ z N Z T
134 simpl2 φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T ¬ w N Z T w V
135 simpl3l φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T ¬ w N Z T ¬ w N Y X
136 135 120 sylnib φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T ¬ w N Z T ¬ w N X Y
137 simpr φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T ¬ w N Z T ¬ w N Z T
138 eleq1 z = w z N X Y w N X Y
139 138 notbid z = w ¬ z N X Y ¬ w N X Y
140 eleq1 z = w z N Z T w N Z T
141 140 notbid z = w ¬ z N Z T ¬ w N Z T
142 139 141 anbi12d z = w ¬ z N X Y ¬ z N Z T ¬ w N X Y ¬ w N Z T
143 142 rspcev w V ¬ w N X Y ¬ w N Z T z V ¬ z N X Y ¬ z N Z T
144 134 136 137 143 syl12anc φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T ¬ w N Z T z V ¬ z N X Y ¬ z N Z T
145 133 144 pm2.61dan φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T z V ¬ z N X Y ¬ z N Z T
146 145 rexlimdv3a φ ¬ Y N Z T w V ¬ w N Y X ¬ w N Y T z V ¬ z N X Y ¬ z N Z T
147 107 146 mpd φ ¬ Y N Z T z V ¬ z N X Y ¬ z N Z T
148 105 147 pm2.61dan φ z V ¬ z N X Y ¬ z N Z T