Step | Hyp | Ref
| Expression |
1 | | n0 4280 |
. . . . . 6
⊢ ((𝑈 ∖ { 0 }) ≠ ∅ ↔
∃𝑥 𝑥 ∈ (𝑈 ∖ { 0 })) |
2 | | simprl 768 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑈 ⊆ (𝑁‘{𝑋})) |
3 | | lspsnat.s |
. . . . . . . . . 10
⊢ 𝑆 = (LSubSp‘𝑊) |
4 | | lspsnat.n |
. . . . . . . . . 10
⊢ 𝑁 = (LSpan‘𝑊) |
5 | | simpl1 1190 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑊 ∈ LVec) |
6 | | lveclmod 20368 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑊 ∈ LMod) |
8 | | simpl2 1191 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑈 ∈ 𝑆) |
9 | | simprr 770 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑥 ∈ (𝑈 ∖ { 0 })) |
10 | 9 | eldifad 3899 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑥 ∈ 𝑈) |
11 | 3, 4, 7, 8, 10 | lspsnel5a 20258 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → (𝑁‘{𝑥}) ⊆ 𝑈) |
12 | | 0ss 4330 |
. . . . . . . . . . . . . 14
⊢ ∅
⊆ 𝑉 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → ∅
⊆ 𝑉) |
14 | | simpl3 1192 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑋 ∈ 𝑉) |
15 | | ssdif 4074 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ⊆ (𝑁‘{𝑋}) → (𝑈 ∖ { 0 }) ⊆ ((𝑁‘{𝑋}) ∖ { 0 })) |
16 | 15 | ad2antrl 725 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → (𝑈 ∖ { 0 }) ⊆ ((𝑁‘{𝑋}) ∖ { 0 })) |
17 | 16, 9 | sseldd 3922 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑥 ∈ ((𝑁‘{𝑋}) ∖ { 0 })) |
18 | | uncom 4087 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅
∪ {𝑋}) = ({𝑋} ∪
∅) |
19 | | un0 4324 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑋} ∪ ∅) = {𝑋} |
20 | 18, 19 | eqtri 2766 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∪ {𝑋}) = {𝑋} |
21 | 20 | fveq2i 6777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁‘(∅ ∪ {𝑋})) = (𝑁‘{𝑋}) |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → (𝑁‘(∅ ∪ {𝑋})) = (𝑁‘{𝑋})) |
23 | | lspsnat.z |
. . . . . . . . . . . . . . . . 17
⊢ 0 =
(0g‘𝑊) |
24 | 23, 4 | lsp0 20271 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod → (𝑁‘∅) = { 0
}) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → (𝑁‘∅) = { 0
}) |
26 | 22, 25 | difeq12d 4058 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → ((𝑁‘(∅ ∪ {𝑋})) ∖ (𝑁‘∅)) = ((𝑁‘{𝑋}) ∖ { 0 })) |
27 | 17, 26 | eleqtrrd 2842 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑥 ∈ ((𝑁‘(∅ ∪ {𝑋})) ∖ (𝑁‘∅))) |
28 | | lspsnat.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (Base‘𝑊) |
29 | 28, 3, 4 | lspsolv 20405 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ (∅
⊆ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ ((𝑁‘(∅ ∪ {𝑋})) ∖ (𝑁‘∅)))) → 𝑋 ∈ (𝑁‘(∅ ∪ {𝑥}))) |
30 | 5, 13, 14, 27, 29 | syl13anc 1371 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑋 ∈ (𝑁‘(∅ ∪ {𝑥}))) |
31 | | uncom 4087 |
. . . . . . . . . . . . . 14
⊢ (∅
∪ {𝑥}) = ({𝑥} ∪
∅) |
32 | | un0 4324 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ∪ ∅) = {𝑥} |
33 | 31, 32 | eqtri 2766 |
. . . . . . . . . . . . 13
⊢ (∅
∪ {𝑥}) = {𝑥} |
34 | 33 | fveq2i 6777 |
. . . . . . . . . . . 12
⊢ (𝑁‘(∅ ∪ {𝑥})) = (𝑁‘{𝑥}) |
35 | 30, 34 | eleqtrdi 2849 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑋 ∈ (𝑁‘{𝑥})) |
36 | 11, 35 | sseldd 3922 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑋 ∈ 𝑈) |
37 | 3, 4, 7, 8, 36 | lspsnel5a 20258 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → (𝑁‘{𝑋}) ⊆ 𝑈) |
38 | 2, 37 | eqssd 3938 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ (𝑈 ⊆ (𝑁‘{𝑋}) ∧ 𝑥 ∈ (𝑈 ∖ { 0 }))) → 𝑈 = (𝑁‘{𝑋})) |
39 | 38 | expr 457 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑥 ∈ (𝑈 ∖ { 0 }) → 𝑈 = (𝑁‘{𝑋}))) |
40 | 39 | exlimdv 1936 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (∃𝑥 𝑥 ∈ (𝑈 ∖ { 0 }) → 𝑈 = (𝑁‘{𝑋}))) |
41 | 1, 40 | syl5bi 241 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → ((𝑈 ∖ { 0 }) ≠ ∅ →
𝑈 = (𝑁‘{𝑋}))) |
42 | 41 | necon1bd 2961 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (¬ 𝑈 = (𝑁‘{𝑋}) → (𝑈 ∖ { 0 }) =
∅)) |
43 | | ssdif0 4297 |
. . . 4
⊢ (𝑈 ⊆ { 0 } ↔ (𝑈 ∖ { 0 }) =
∅) |
44 | 42, 43 | syl6ibr 251 |
. . 3
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (¬ 𝑈 = (𝑁‘{𝑋}) → 𝑈 ⊆ { 0 })) |
45 | | simpl1 1190 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → 𝑊 ∈ LVec) |
46 | 45, 6 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → 𝑊 ∈ LMod) |
47 | | simpl2 1191 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → 𝑈 ∈ 𝑆) |
48 | 23, 3 | lssle0 20211 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑈 ⊆ { 0 } ↔ 𝑈 = { 0 })) |
49 | 46, 47, 48 | syl2anc 584 |
. . 3
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑈 ⊆ { 0 } ↔ 𝑈 = { 0 })) |
50 | 44, 49 | sylibd 238 |
. 2
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (¬ 𝑈 = (𝑁‘{𝑋}) → 𝑈 = { 0 })) |
51 | 50 | orrd 860 |
1
⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑈 = (𝑁‘{𝑋}) ∨ 𝑈 = { 0 })) |