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