Description: The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lshpnelb.v | |
|
lshpnelb.n | |
||
lshpnelb.p | |
||
lshpnelb.h | |
||
lshpnelb.w | |
||
lshpnelb.u | |
||
lshpnelb.x | |
||
Assertion | lshpnelb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lshpnelb.v | |
|
2 | lshpnelb.n | |
|
3 | lshpnelb.p | |
|
4 | lshpnelb.h | |
|
5 | lshpnelb.w | |
|
6 | lshpnelb.u | |
|
7 | lshpnelb.x | |
|
8 | eqid | |
|
9 | lveclmod | |
|
10 | 5 9 | syl | |
11 | 1 2 8 3 4 10 | islshpsm | |
12 | 6 11 | mpbid | |
13 | 12 | simp3d | |
14 | 13 | adantr | |
15 | simp1l | |
|
16 | simp2 | |
|
17 | 8 | lsssssubg | |
18 | 10 17 | syl | |
19 | 8 4 10 6 | lshplss | |
20 | 18 19 | sseldd | |
21 | 1 8 2 | lspsncl | |
22 | 10 7 21 | syl2anc | |
23 | 18 22 | sseldd | |
24 | 3 | lsmub1 | |
25 | 20 23 24 | syl2anc | |
26 | 25 | adantr | |
27 | 3 | lsmub2 | |
28 | 20 23 27 | syl2anc | |
29 | 1 2 | lspsnid | |
30 | 10 7 29 | syl2anc | |
31 | 28 30 | sseldd | |
32 | nelne1 | |
|
33 | 31 32 | sylan | |
34 | 33 | necomd | |
35 | df-pss | |
|
36 | 26 34 35 | sylanbrc | |
37 | 36 | 3ad2ant1 | |
38 | 8 3 | lsmcl | |
39 | 10 19 22 38 | syl3anc | |
40 | 1 8 | lssss | |
41 | 39 40 | syl | |
42 | 41 | adantr | |
43 | simpr | |
|
44 | 42 43 | sseqtrrd | |
45 | 44 | adantlr | |
46 | 45 | 3adant2 | |
47 | 5 | adantr | |
48 | 19 | adantr | |
49 | 39 | adantr | |
50 | simpr | |
|
51 | 1 8 2 3 47 48 49 50 | lsmcv | |
52 | 15 16 37 46 51 | syl211anc | |
53 | simp3 | |
|
54 | 52 53 | eqtrd | |
55 | 54 | rexlimdv3a | |
56 | 14 55 | mpd | |
57 | 10 | adantr | |
58 | 6 | adantr | |
59 | 7 | adantr | |
60 | simpr | |
|
61 | 1 2 3 4 57 58 59 60 | lshpnel | |
62 | 56 61 | impbida | |