Step | Hyp | Ref
| Expression |
1 | | lveclmod 20939 |
. . . . 5
β’ (π β LVec β π β LMod) |
2 | | snssi 4803 |
. . . . 5
β’ (π β π β {π} β π) |
3 | | lbslsat.v |
. . . . . 6
β’ π = (Baseβπ) |
4 | | eqid 2724 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
5 | | lbslsat.n |
. . . . . 6
β’ π = (LSpanβπ) |
6 | 3, 4, 5 | lspcl 20808 |
. . . . 5
β’ ((π β LMod β§ {π} β π) β (πβ{π}) β (LSubSpβπ)) |
7 | 1, 2, 6 | syl2an 595 |
. . . 4
β’ ((π β LVec β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
8 | | lbslsat.y |
. . . . 5
β’ π = (π βΎs (πβ{π})) |
9 | 8, 4 | lsslvec 20942 |
. . . 4
β’ ((π β LVec β§ (πβ{π}) β (LSubSpβπ)) β π β LVec) |
10 | 7, 9 | syldan 590 |
. . 3
β’ ((π β LVec β§ π β π) β π β LVec) |
11 | 10 | 3adant3 1129 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β π β LVec) |
12 | 3, 5 | lspssid 20817 |
. . . . 5
β’ ((π β LMod β§ {π} β π) β {π} β (πβ{π})) |
13 | 1, 2, 12 | syl2an 595 |
. . . 4
β’ ((π β LVec β§ π β π) β {π} β (πβ{π})) |
14 | 3, 5 | lspssv 20815 |
. . . . . 6
β’ ((π β LMod β§ {π} β π) β (πβ{π}) β π) |
15 | 1, 2, 14 | syl2an 595 |
. . . . 5
β’ ((π β LVec β§ π β π) β (πβ{π}) β π) |
16 | 8, 3 | ressbas2 17178 |
. . . . 5
β’ ((πβ{π}) β π β (πβ{π}) = (Baseβπ)) |
17 | 15, 16 | syl 17 |
. . . 4
β’ ((π β LVec β§ π β π) β (πβ{π}) = (Baseβπ)) |
18 | 13, 17 | sseqtrd 4014 |
. . 3
β’ ((π β LVec β§ π β π) β {π} β (Baseβπ)) |
19 | 18 | 3adant3 1129 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (Baseβπ)) |
20 | 1 | adantr 480 |
. . . . 5
β’ ((π β LVec β§ π β π) β π β LMod) |
21 | | eqid 2724 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
22 | 8, 5, 21, 4 | lsslsp 20847 |
. . . . 5
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ {π} β (πβ{π})) β ((LSpanβπ)β{π}) = (πβ{π})) |
23 | 20, 7, 13, 22 | syl3anc 1368 |
. . . 4
β’ ((π β LVec β§ π β π) β ((LSpanβπ)β{π}) = (πβ{π})) |
24 | 23 | 3adant3 1129 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β
((LSpanβπ)β{π}) = (πβ{π})) |
25 | 17 | 3adant3 1129 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β (πβ{π}) = (Baseβπ)) |
26 | 24, 25 | eqtrd 2764 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β
((LSpanβπ)β{π}) = (Baseβπ)) |
27 | | difid 4362 |
. . . . . . . . . . . . 13
β’ ({π} β {π}) = β
|
28 | 27 | fveq2i 6884 |
. . . . . . . . . . . 12
β’
((LSpanβπ)β({π} β {π})) = ((LSpanβπ)ββ
) |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β LVec β§ π β π) β ((LSpanβπ)β({π} β {π})) = ((LSpanβπ)ββ
)) |
30 | 29 | eleq2d 2811 |
. . . . . . . . . 10
β’ ((π β LVec β§ π β π) β (π β ((LSpanβπ)β({π} β {π})) β π β ((LSpanβπ)ββ
))) |
31 | 30 | biimpa 476 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π β ((LSpanβπ)ββ
)) |
32 | | lveclmod 20939 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
33 | | eqid 2724 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
34 | 33, 21 | lsp0 20841 |
. . . . . . . . . . 11
β’ (π β LMod β
((LSpanβπ)ββ
) =
{(0gβπ)}) |
35 | 10, 32, 34 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β LVec β§ π β π) β ((LSpanβπ)ββ
) =
{(0gβπ)}) |
36 | 35 | adantr 480 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β ((LSpanβπ)ββ
) =
{(0gβπ)}) |
37 | 31, 36 | eleqtrd 2827 |
. . . . . . . 8
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π β {(0gβπ)}) |
38 | | elsni 4637 |
. . . . . . . 8
β’ (π β
{(0gβπ)}
β π =
(0gβπ)) |
39 | 37, 38 | syl 17 |
. . . . . . 7
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π = (0gβπ)) |
40 | | lmodgrp 20698 |
. . . . . . . . . 10
β’ (π β LMod β π β Grp) |
41 | | grpmnd 18857 |
. . . . . . . . . 10
β’ (π β Grp β π β Mnd) |
42 | 20, 40, 41 | 3syl 18 |
. . . . . . . . 9
β’ ((π β LVec β§ π β π) β π β Mnd) |
43 | | lbslsat.z |
. . . . . . . . . . 11
β’ 0 =
(0gβπ) |
44 | 43, 3, 5 | 0ellsp 32913 |
. . . . . . . . . 10
β’ ((π β LMod β§ {π} β π) β 0 β (πβ{π})) |
45 | 1, 2, 44 | syl2an 595 |
. . . . . . . . 9
β’ ((π β LVec β§ π β π) β 0 β (πβ{π})) |
46 | 8, 3, 43 | ress0g 18682 |
. . . . . . . . 9
β’ ((π β Mnd β§ 0 β (πβ{π}) β§ (πβ{π}) β π) β 0 =
(0gβπ)) |
47 | 42, 45, 15, 46 | syl3anc 1368 |
. . . . . . . 8
β’ ((π β LVec β§ π β π) β 0 =
(0gβπ)) |
48 | 47 | adantr 480 |
. . . . . . 7
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β 0 =
(0gβπ)) |
49 | 39, 48 | eqtr4d 2767 |
. . . . . 6
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π = 0 ) |
50 | 49 | ex 412 |
. . . . 5
β’ ((π β LVec β§ π β π) β (π β ((LSpanβπ)β({π} β {π})) β π = 0 )) |
51 | 50 | necon3ad 2945 |
. . . 4
β’ ((π β LVec β§ π β π) β (π β 0 β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
52 | 51 | 3impia 1114 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β Β¬ π β ((LSpanβπ)β({π} β {π}))) |
53 | | id 22 |
. . . . . . 7
β’ (π₯ = π β π₯ = π) |
54 | | sneq 4630 |
. . . . . . . . 9
β’ (π₯ = π β {π₯} = {π}) |
55 | 54 | difeq2d 4114 |
. . . . . . . 8
β’ (π₯ = π β ({π} β {π₯}) = ({π} β {π})) |
56 | 55 | fveq2d 6885 |
. . . . . . 7
β’ (π₯ = π β ((LSpanβπ)β({π} β {π₯})) = ((LSpanβπ)β({π} β {π}))) |
57 | 53, 56 | eleq12d 2819 |
. . . . . 6
β’ (π₯ = π β (π₯ β ((LSpanβπ)β({π} β {π₯})) β π β ((LSpanβπ)β({π} β {π})))) |
58 | 57 | notbid 318 |
. . . . 5
β’ (π₯ = π β (Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
59 | 58 | ralsng 4669 |
. . . 4
β’ (π β π β (βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
60 | 59 | 3ad2ant2 1131 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β (βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
61 | 52, 60 | mpbird 257 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯}))) |
62 | | eqid 2724 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
63 | | eqid 2724 |
. . . 4
β’
(LBasisβπ) =
(LBasisβπ) |
64 | 62, 63, 21 | islbs2 20990 |
. . 3
β’ (π β LVec β ({π} β (LBasisβπ) β ({π} β (Baseβπ) β§ ((LSpanβπ)β{π}) = (Baseβπ) β§ βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯}))))) |
65 | 64 | biimpar 477 |
. 2
β’ ((π β LVec β§ ({π} β (Baseβπ) β§ ((LSpanβπ)β{π}) = (Baseβπ) β§ βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})))) β {π} β (LBasisβπ)) |
66 | 11, 19, 26, 61, 65 | syl13anc 1369 |
1
β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (LBasisβπ)) |