Step | Hyp | Ref
| Expression |
1 | | n0 4347 |
. . . . . 6
β’ ((π β { 0 }) β β
β
βπ₯ π₯ β (π β { 0 })) |
2 | | simprl 770 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β (πβ{π})) |
3 | | lspsnat.s |
. . . . . . . . . 10
β’ π = (LSubSpβπ) |
4 | | lspsnat.n |
. . . . . . . . . 10
β’ π = (LSpanβπ) |
5 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β LVec) |
6 | | lveclmod 20717 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β LMod) |
8 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β π) |
9 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β (π β { 0 })) |
10 | 9 | eldifad 3961 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β π) |
11 | 3, 4, 7, 8, 10 | lspsnel5a 20607 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πβ{π₯}) β π) |
12 | | 0ss 4397 |
. . . . . . . . . . . . . 14
β’ β
β π |
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β β
β π) |
14 | | simpl3 1194 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β π) |
15 | | ssdif 4140 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ{π}) β (π β { 0 }) β ((πβ{π}) β { 0 })) |
16 | 15 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (π β { 0 }) β ((πβ{π}) β { 0 })) |
17 | 16, 9 | sseldd 3984 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β ((πβ{π}) β { 0 })) |
18 | | uncom 4154 |
. . . . . . . . . . . . . . . . . 18
β’ (β
βͺ {π}) = ({π} βͺ
β
) |
19 | | un0 4391 |
. . . . . . . . . . . . . . . . . 18
β’ ({π} βͺ β
) = {π} |
20 | 18, 19 | eqtri 2761 |
. . . . . . . . . . . . . . . . 17
β’ (β
βͺ {π}) = {π} |
21 | 20 | fveq2i 6895 |
. . . . . . . . . . . . . . . 16
β’ (πβ(β
βͺ {π})) = (πβ{π}) |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πβ(β
βͺ {π})) = (πβ{π})) |
23 | | lspsnat.z |
. . . . . . . . . . . . . . . . 17
β’ 0 =
(0gβπ) |
24 | 23, 4 | lsp0 20620 |
. . . . . . . . . . . . . . . 16
β’ (π β LMod β (πββ
) = { 0
}) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πββ
) = { 0
}) |
26 | 22, 25 | difeq12d 4124 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β ((πβ(β
βͺ {π})) β (πββ
)) = ((πβ{π}) β { 0 })) |
27 | 17, 26 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β ((πβ(β
βͺ {π})) β (πββ
))) |
28 | | lspsnat.v |
. . . . . . . . . . . . . 14
β’ π = (Baseβπ) |
29 | 28, 3, 4 | lspsolv 20756 |
. . . . . . . . . . . . 13
β’ ((π β LVec β§ (β
β π β§ π β π β§ π₯ β ((πβ(β
βͺ {π})) β (πββ
)))) β π β (πβ(β
βͺ {π₯}))) |
30 | 5, 13, 14, 27, 29 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β (πβ(β
βͺ {π₯}))) |
31 | | uncom 4154 |
. . . . . . . . . . . . . 14
β’ (β
βͺ {π₯}) = ({π₯} βͺ
β
) |
32 | | un0 4391 |
. . . . . . . . . . . . . 14
β’ ({π₯} βͺ β
) = {π₯} |
33 | 31, 32 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ (β
βͺ {π₯}) = {π₯} |
34 | 33 | fveq2i 6895 |
. . . . . . . . . . . 12
β’ (πβ(β
βͺ {π₯})) = (πβ{π₯}) |
35 | 30, 34 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β (πβ{π₯})) |
36 | 11, 35 | sseldd 3984 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β π) |
37 | 3, 4, 7, 8, 36 | lspsnel5a 20607 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πβ{π}) β π) |
38 | 2, 37 | eqssd 4000 |
. . . . . . . 8
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π = (πβ{π})) |
39 | 38 | expr 458 |
. . . . . . 7
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (π₯ β (π β { 0 }) β π = (πβ{π}))) |
40 | 39 | exlimdv 1937 |
. . . . . 6
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (βπ₯ π₯ β (π β { 0 }) β π = (πβ{π}))) |
41 | 1, 40 | biimtrid 241 |
. . . . 5
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β ((π β { 0 }) β β
β
π = (πβ{π}))) |
42 | 41 | necon1bd 2959 |
. . . 4
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (Β¬ π = (πβ{π}) β (π β { 0 }) =
β
)) |
43 | | ssdif0 4364 |
. . . 4
β’ (π β { 0 } β (π β { 0 }) =
β
) |
44 | 42, 43 | imbitrrdi 251 |
. . 3
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (Β¬ π = (πβ{π}) β π β { 0 })) |
45 | | simpl1 1192 |
. . . . 5
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β π β LVec) |
46 | 45, 6 | syl 17 |
. . . 4
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β π β LMod) |
47 | | simpl2 1193 |
. . . 4
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β π β π) |
48 | 23, 3 | lssle0 20560 |
. . . 4
β’ ((π β LMod β§ π β π) β (π β { 0 } β π = { 0 })) |
49 | 46, 47, 48 | syl2anc 585 |
. . 3
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (π β { 0 } β π = { 0 })) |
50 | 44, 49 | sylibd 238 |
. 2
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (Β¬ π = (πβ{π}) β π = { 0 })) |
51 | 50 | orrd 862 |
1
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (π = (πβ{π}) β¨ π = { 0 })) |