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 𝑉 = ( Base ‘ 𝑊 )
lspsnat.z 0 = ( 0g𝑊 )
lspsnat.s 𝑆 = ( LSubSp ‘ 𝑊 )
lspsnat.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsnat ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑈 = { 0 } ) )

Proof

Step Hyp Ref Expression
1 lspsnat.v 𝑉 = ( Base ‘ 𝑊 )
2 lspsnat.z 0 = ( 0g𝑊 )
3 lspsnat.s 𝑆 = ( LSubSp ‘ 𝑊 )
4 lspsnat.n 𝑁 = ( LSpan ‘ 𝑊 )
5 n0 ( ( 𝑈 ∖ { 0 } ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
6 simprl ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) )
7 simpl1 ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑊 ∈ LVec )
8 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 7 8 syl ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑊 ∈ LMod )
10 simpl2 ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑈𝑆 )
11 simprr ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
12 11 eldifad ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑥𝑈 )
13 3 4 9 10 12 lspsnel5a ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ 𝑈 )
14 0ss ∅ ⊆ 𝑉
15 14 a1i ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → ∅ ⊆ 𝑉 )
16 simpl3 ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑋𝑉 )
17 ssdif ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) → ( 𝑈 ∖ { 0 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ∖ { 0 } ) )
18 17 ad2antrl ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → ( 𝑈 ∖ { 0 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ∖ { 0 } ) )
19 18 11 sseldd ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑥 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∖ { 0 } ) )
20 uncom ( ∅ ∪ { 𝑋 } ) = ( { 𝑋 } ∪ ∅ )
21 un0 ( { 𝑋 } ∪ ∅ ) = { 𝑋 }
22 20 21 eqtri ( ∅ ∪ { 𝑋 } ) = { 𝑋 }
23 22 fveq2i ( 𝑁 ‘ ( ∅ ∪ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } )
24 23 a1i ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → ( 𝑁 ‘ ( ∅ ∪ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
25 2 4 lsp0 ( 𝑊 ∈ LMod → ( 𝑁 ‘ ∅ ) = { 0 } )
26 9 25 syl ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → ( 𝑁 ‘ ∅ ) = { 0 } )
27 24 26 difeq12d ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → ( ( 𝑁 ‘ ( ∅ ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ ∅ ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ∖ { 0 } ) )
28 19 27 eleqtrrd ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑥 ∈ ( ( 𝑁 ‘ ( ∅ ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ ∅ ) ) )
29 1 3 4 lspsolv ( ( 𝑊 ∈ LVec ∧ ( ∅ ⊆ 𝑉𝑋𝑉𝑥 ∈ ( ( 𝑁 ‘ ( ∅ ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ ∅ ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( ∅ ∪ { 𝑥 } ) ) )
30 7 15 16 28 29 syl13anc ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( ∅ ∪ { 𝑥 } ) ) )
31 uncom ( ∅ ∪ { 𝑥 } ) = ( { 𝑥 } ∪ ∅ )
32 un0 ( { 𝑥 } ∪ ∅ ) = { 𝑥 }
33 31 32 eqtri ( ∅ ∪ { 𝑥 } ) = { 𝑥 }
34 33 fveq2i ( 𝑁 ‘ ( ∅ ∪ { 𝑥 } ) ) = ( 𝑁 ‘ { 𝑥 } )
35 30 34 eleqtrdi ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 } ) )
36 13 35 sseldd ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑋𝑈 )
37 3 4 9 10 36 lspsnel5a ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
38 6 37 eqssd ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) ) → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) )
39 38 expr ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) )
40 39 exlimdv ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ∃ 𝑥 𝑥 ∈ ( 𝑈 ∖ { 0 } ) → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) )
41 5 40 syl5bi ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ( 𝑈 ∖ { 0 } ) ≠ ∅ → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) )
42 41 necon1bd ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ¬ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) → ( 𝑈 ∖ { 0 } ) = ∅ ) )
43 ssdif0 ( 𝑈 ⊆ { 0 } ↔ ( 𝑈 ∖ { 0 } ) = ∅ )
44 42 43 syl6ibr ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ¬ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) → 𝑈 ⊆ { 0 } ) )
45 simpl1 ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑊 ∈ LVec )
46 45 8 syl ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑊 ∈ LMod )
47 simpl2 ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑈𝑆 )
48 2 3 lssle0 ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑈 ⊆ { 0 } ↔ 𝑈 = { 0 } ) )
49 46 47 48 syl2anc ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑈 ⊆ { 0 } ↔ 𝑈 = { 0 } ) )
50 44 49 sylibd ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ¬ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) → 𝑈 = { 0 } ) )
51 50 orrd ( ( ( 𝑊 ∈ LVec ∧ 𝑈𝑆𝑋𝑉 ) ∧ 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑈 = { 0 } ) )