Metamath Proof Explorer

Theorem lspsnat

Description: There is no subspace strictly between the zero subspace and the span of a vector (i.e. a 1-dimensional subspace is an atom). ( h1datomi analog.) (Contributed by NM, 20-Apr-2014) (Proof shortened by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses lspsnat.v 
|- V = ( Base ` W )
lspsnat.z 
|- .0. = ( 0g ` W )
lspsnat.s 
|- S = ( LSubSp ` W )
lspsnat.n 
|- N = ( LSpan ` W )
Assertion lspsnat 
|- ( ( ( W e. LVec /\ U e. S /\ X e. V ) /\ U C_ ( N ` { X } ) ) -> ( U = ( N ` { X } ) \/ U = { .0. } ) )

Proof

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. } ) )