Step |
Hyp |
Ref |
Expression |
1 |
|
lspsnat.v |
|- V = ( Base ` W ) |
2 |
|
lspsnat.z |
|- .0. = ( 0g ` W ) |
3 |
|
lspsnat.s |
|- S = ( LSubSp ` W ) |
4 |
|
lspsnat.n |
|- N = ( LSpan ` W ) |
5 |
|
n0 |
|- ( ( U \ { .0. } ) =/= (/) <-> E. x x e. ( U \ { .0. } ) ) |
6 |
|
simprl |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> U C_ ( N ` { X } ) ) |
7 |
|
simpl1 |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> W e. LVec ) |
8 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
9 |
7 8
|
syl |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> W e. LMod ) |
10 |
|
simpl2 |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> U e. S ) |
11 |
|
simprr |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> x e. ( U \ { .0. } ) ) |
12 |
11
|
eldifad |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> x e. U ) |
13 |
3 4 9 10 12
|
lspsnel5a |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> ( N ` { x } ) C_ U ) |
14 |
|
0ss |
|- (/) C_ V |
15 |
14
|
a1i |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> (/) C_ V ) |
16 |
|
simpl3 |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> X e. V ) |
17 |
|
ssdif |
|- ( U C_ ( N ` { X } ) -> ( U \ { .0. } ) C_ ( ( N ` { X } ) \ { .0. } ) ) |
18 |
17
|
ad2antrl |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> ( U \ { .0. } ) C_ ( ( N ` { X } ) \ { .0. } ) ) |
19 |
18 11
|
sseldd |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> x e. ( ( N ` { X } ) \ { .0. } ) ) |
20 |
|
uncom |
|- ( (/) u. { X } ) = ( { X } u. (/) ) |
21 |
|
un0 |
|- ( { X } u. (/) ) = { X } |
22 |
20 21
|
eqtri |
|- ( (/) u. { X } ) = { X } |
23 |
22
|
fveq2i |
|- ( N ` ( (/) u. { X } ) ) = ( N ` { X } ) |
24 |
23
|
a1i |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> ( N ` ( (/) u. { X } ) ) = ( N ` { X } ) ) |
25 |
2 4
|
lsp0 |
|- ( W e. LMod -> ( N ` (/) ) = { .0. } ) |
26 |
9 25
|
syl |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> ( N ` (/) ) = { .0. } ) |
27 |
24 26
|
difeq12d |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> ( ( N ` ( (/) u. { X } ) ) \ ( N ` (/) ) ) = ( ( N ` { X } ) \ { .0. } ) ) |
28 |
19 27
|
eleqtrrd |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> x e. ( ( N ` ( (/) u. { X } ) ) \ ( N ` (/) ) ) ) |
29 |
1 3 4
|
lspsolv |
|- ( ( W e. LVec /\ ( (/) C_ V /\ X e. V /\ x e. ( ( N ` ( (/) u. { X } ) ) \ ( N ` (/) ) ) ) ) -> X e. ( N ` ( (/) u. { x } ) ) ) |
30 |
7 15 16 28 29
|
syl13anc |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> X e. ( N ` ( (/) u. { x } ) ) ) |
31 |
|
uncom |
|- ( (/) u. { x } ) = ( { x } u. (/) ) |
32 |
|
un0 |
|- ( { x } u. (/) ) = { x } |
33 |
31 32
|
eqtri |
|- ( (/) u. { x } ) = { x } |
34 |
33
|
fveq2i |
|- ( N ` ( (/) u. { x } ) ) = ( N ` { x } ) |
35 |
30 34
|
eleqtrdi |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> X e. ( N ` { x } ) ) |
36 |
13 35
|
sseldd |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> X e. U ) |
37 |
3 4 9 10 36
|
lspsnel5a |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> ( N ` { X } ) C_ U ) |
38 |
6 37
|
eqssd |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ ( U C_ ( N ` { X } ) /\ x e. ( U \ { .0. } ) ) ) -> U = ( N ` { X } ) ) |
39 |
38
|
expr |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( x e. ( U \ { .0. } ) -> U = ( N ` { X } ) ) ) |
40 |
39
|
exlimdv |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( E. x x e. ( U \ { .0. } ) -> U = ( N ` { X } ) ) ) |
41 |
5 40
|
syl5bi |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( ( U \ { .0. } ) =/= (/) -> U = ( N ` { X } ) ) ) |
42 |
41
|
necon1bd |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( -. U = ( N ` { X } ) -> ( U \ { .0. } ) = (/) ) ) |
43 |
|
ssdif0 |
|- ( U C_ { .0. } <-> ( U \ { .0. } ) = (/) ) |
44 |
42 43
|
syl6ibr |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( -. U = ( N ` { X } ) -> U C_ { .0. } ) ) |
45 |
|
simpl1 |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> W e. LVec ) |
46 |
45 8
|
syl |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> W e. LMod ) |
47 |
|
simpl2 |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> U e. S ) |
48 |
2 3
|
lssle0 |
|- ( ( W e. LMod /\ U e. S ) -> ( U C_ { .0. } <-> U = { .0. } ) ) |
49 |
46 47 48
|
syl2anc |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( U C_ { .0. } <-> U = { .0. } ) ) |
50 |
44 49
|
sylibd |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( -. U = ( N ` { X } ) -> U = { .0. } ) ) |
51 |
50
|
orrd |
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( U = ( N ` { X } ) \/ U = { .0. } ) ) |