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