Step | Hyp | Ref
| Expression |
1 | | n0 4346 |
. . . . . 6
β’ ((π β { 0 }) β β
β
βπ₯ π₯ β (π β { 0 })) |
2 | | simprl 769 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β (πβ{π})) |
3 | | lspsnat.s |
. . . . . . . . . 10
β’ π = (LSubSpβπ) |
4 | | lspsnat.n |
. . . . . . . . . 10
β’ π = (LSpanβπ) |
5 | | simpl1 1191 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β LVec) |
6 | | lveclmod 20861 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β LMod) |
8 | | simpl2 1192 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β π) |
9 | | simprr 771 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β (π β { 0 })) |
10 | 9 | eldifad 3960 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β π) |
11 | 3, 4, 7, 8, 10 | lspsnel5a 20751 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πβ{π₯}) β π) |
12 | | 0ss 4396 |
. . . . . . . . . . . . . 14
β’ β
β π |
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β β
β π) |
14 | | simpl3 1193 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β π) |
15 | | ssdif 4139 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ{π}) β (π β { 0 }) β ((πβ{π}) β { 0 })) |
16 | 15 | ad2antrl 726 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (π β { 0 }) β ((πβ{π}) β { 0 })) |
17 | 16, 9 | sseldd 3983 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β ((πβ{π}) β { 0 })) |
18 | | uncom 4153 |
. . . . . . . . . . . . . . . . . 18
β’ (β
βͺ {π}) = ({π} βͺ
β
) |
19 | | un0 4390 |
. . . . . . . . . . . . . . . . . 18
β’ ({π} βͺ β
) = {π} |
20 | 18, 19 | eqtri 2760 |
. . . . . . . . . . . . . . . . 17
β’ (β
βͺ {π}) = {π} |
21 | 20 | fveq2i 6894 |
. . . . . . . . . . . . . . . 16
β’ (πβ(β
βͺ {π})) = (πβ{π}) |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πβ(β
βͺ {π})) = (πβ{π})) |
23 | | lspsnat.z |
. . . . . . . . . . . . . . . . 17
β’ 0 =
(0gβπ) |
24 | 23, 4 | lsp0 20764 |
. . . . . . . . . . . . . . . 16
β’ (π β LMod β (πββ
) = { 0
}) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πββ
) = { 0
}) |
26 | 22, 25 | difeq12d 4123 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β ((πβ(β
βͺ {π})) β (πββ
)) = ((πβ{π}) β { 0 })) |
27 | 17, 26 | eleqtrrd 2836 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π₯ β ((πβ(β
βͺ {π})) β (πββ
))) |
28 | | lspsnat.v |
. . . . . . . . . . . . . 14
β’ π = (Baseβπ) |
29 | 28, 3, 4 | lspsolv 20901 |
. . . . . . . . . . . . 13
β’ ((π β LVec β§ (β
β π β§ π β π β§ π₯ β ((πβ(β
βͺ {π})) β (πββ
)))) β π β (πβ(β
βͺ {π₯}))) |
30 | 5, 13, 14, 27, 29 | syl13anc 1372 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β (πβ(β
βͺ {π₯}))) |
31 | | uncom 4153 |
. . . . . . . . . . . . . 14
β’ (β
βͺ {π₯}) = ({π₯} βͺ
β
) |
32 | | un0 4390 |
. . . . . . . . . . . . . 14
β’ ({π₯} βͺ β
) = {π₯} |
33 | 31, 32 | eqtri 2760 |
. . . . . . . . . . . . 13
β’ (β
βͺ {π₯}) = {π₯} |
34 | 33 | fveq2i 6894 |
. . . . . . . . . . . 12
β’ (πβ(β
βͺ {π₯})) = (πβ{π₯}) |
35 | 30, 34 | eleqtrdi 2843 |
. . . . . . . . . . 11
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β (πβ{π₯})) |
36 | 11, 35 | sseldd 3983 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π β π) |
37 | 3, 4, 7, 8, 36 | lspsnel5a 20751 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β (πβ{π}) β π) |
38 | 2, 37 | eqssd 3999 |
. . . . . . . 8
β’ (((π β LVec β§ π β π β§ π β π) β§ (π β (πβ{π}) β§ π₯ β (π β { 0 }))) β π = (πβ{π})) |
39 | 38 | expr 457 |
. . . . . . 7
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (π₯ β (π β { 0 }) β π = (πβ{π}))) |
40 | 39 | exlimdv 1936 |
. . . . . 6
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (βπ₯ π₯ β (π β { 0 }) β π = (πβ{π}))) |
41 | 1, 40 | biimtrid 241 |
. . . . 5
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β ((π β { 0 }) β β
β
π = (πβ{π}))) |
42 | 41 | necon1bd 2958 |
. . . 4
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (Β¬ π = (πβ{π}) β (π β { 0 }) =
β
)) |
43 | | ssdif0 4363 |
. . . 4
β’ (π β { 0 } β (π β { 0 }) =
β
) |
44 | 42, 43 | imbitrrdi 251 |
. . 3
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (Β¬ π = (πβ{π}) β π β { 0 })) |
45 | | simpl1 1191 |
. . . . 5
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β π β LVec) |
46 | 45, 6 | syl 17 |
. . . 4
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β π β LMod) |
47 | | simpl2 1192 |
. . . 4
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β π β π) |
48 | 23, 3 | lssle0 20704 |
. . . 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 861 |
1
β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (π = (πβ{π}) β¨ π = { 0 })) |