Description: No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lbsind2.j | |
|
lbsind2.n | |
||
lbsind2.f | |
||
lbsind2.o | |
||
lbsind2.z | |
||
lbspss.v | |
||
Assertion | lbspss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lbsind2.j | |
|
2 | lbsind2.n | |
|
3 | lbsind2.f | |
|
4 | lbsind2.o | |
|
5 | lbsind2.z | |
|
6 | lbspss.v | |
|
7 | pssnel | |
|
8 | 7 | 3ad2ant3 | |
9 | simpl2 | |
|
10 | 6 1 | lbsss | |
11 | 9 10 | syl | |
12 | simprl | |
|
13 | 11 12 | sseldd | |
14 | simpl1l | |
|
15 | 11 | ssdifssd | |
16 | simpl3 | |
|
17 | 16 | pssssd | |
18 | 17 | sseld | |
19 | simprr | |
|
20 | eleq1w | |
|
21 | 20 | notbid | |
22 | 19 21 | syl5ibrcom | |
23 | 22 | necon2ad | |
24 | 18 23 | jcad | |
25 | eldifsn | |
|
26 | 24 25 | syl6ibr | |
27 | 26 | ssrdv | |
28 | 6 2 | lspss | |
29 | 14 15 27 28 | syl3anc | |
30 | simpl1r | |
|
31 | 1 2 3 4 5 | lbsind2 | |
32 | 14 30 9 12 31 | syl211anc | |
33 | 29 32 | ssneldd | |
34 | nelne1 | |
|
35 | 13 33 34 | syl2anc | |
36 | 35 | necomd | |
37 | 8 36 | exlimddv | |