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