| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lveclmod 20984 |
. . . . 5
β’ (π β LVec β π β LMod) |
| 2 | | snssi 4807 |
. . . . 5
β’ (π β π β {π} β π) |
| 3 | | lbslsat.v |
. . . . . 6
β’ π = (Baseβπ) |
| 4 | | eqid 2728 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 5 | | lbslsat.n |
. . . . . 6
β’ π = (LSpanβπ) |
| 6 | 3, 4, 5 | lspcl 20853 |
. . . . 5
β’ ((π β LMod β§ {π} β π) β (πβ{π}) β (LSubSpβπ)) |
| 7 | 1, 2, 6 | syl2an 595 |
. . . 4
β’ ((π β LVec β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 8 | | lbslsat.y |
. . . . 5
β’ π = (π βΎs (πβ{π})) |
| 9 | 8, 4 | lsslvec 20987 |
. . . 4
β’ ((π β LVec β§ (πβ{π}) β (LSubSpβπ)) β π β LVec) |
| 10 | 7, 9 | syldan 590 |
. . 3
β’ ((π β LVec β§ π β π) β π β LVec) |
| 11 | 10 | 3adant3 1130 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β π β LVec) |
| 12 | 3, 5 | lspssid 20862 |
. . . . 5
β’ ((π β LMod β§ {π} β π) β {π} β (πβ{π})) |
| 13 | 1, 2, 12 | syl2an 595 |
. . . 4
β’ ((π β LVec β§ π β π) β {π} β (πβ{π})) |
| 14 | 3, 5 | lspssv 20860 |
. . . . . 6
β’ ((π β LMod β§ {π} β π) β (πβ{π}) β π) |
| 15 | 1, 2, 14 | syl2an 595 |
. . . . 5
β’ ((π β LVec β§ π β π) β (πβ{π}) β π) |
| 16 | 8, 3 | ressbas2 17211 |
. . . . 5
β’ ((πβ{π}) β π β (πβ{π}) = (Baseβπ)) |
| 17 | 15, 16 | syl 17 |
. . . 4
β’ ((π β LVec β§ π β π) β (πβ{π}) = (Baseβπ)) |
| 18 | 13, 17 | sseqtrd 4018 |
. . 3
β’ ((π β LVec β§ π β π) β {π} β (Baseβπ)) |
| 19 | 18 | 3adant3 1130 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (Baseβπ)) |
| 20 | 1 | adantr 480 |
. . . . 5
β’ ((π β LVec β§ π β π) β π β LMod) |
| 21 | | eqid 2728 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
| 22 | 8, 5, 21, 4 | lsslsp 20892 |
. . . . 5
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ {π} β (πβ{π})) β ((LSpanβπ)β{π}) = (πβ{π})) |
| 23 | 20, 7, 13, 22 | syl3anc 1369 |
. . . 4
β’ ((π β LVec β§ π β π) β ((LSpanβπ)β{π}) = (πβ{π})) |
| 24 | 23 | 3adant3 1130 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β
((LSpanβπ)β{π}) = (πβ{π})) |
| 25 | 17 | 3adant3 1130 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β (πβ{π}) = (Baseβπ)) |
| 26 | 24, 25 | eqtrd 2768 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β
((LSpanβπ)β{π}) = (Baseβπ)) |
| 27 | | difid 4366 |
. . . . . . . . . . . . 13
β’ ({π} β {π}) = β
|
| 28 | 27 | fveq2i 6894 |
. . . . . . . . . . . 12
β’
((LSpanβπ)β({π} β {π})) = ((LSpanβπ)ββ
) |
| 29 | 28 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β LVec β§ π β π) β ((LSpanβπ)β({π} β {π})) = ((LSpanβπ)ββ
)) |
| 30 | 29 | eleq2d 2815 |
. . . . . . . . . 10
β’ ((π β LVec β§ π β π) β (π β ((LSpanβπ)β({π} β {π})) β π β ((LSpanβπ)ββ
))) |
| 31 | 30 | biimpa 476 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π β ((LSpanβπ)ββ
)) |
| 32 | | lveclmod 20984 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
| 33 | | eqid 2728 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
| 34 | 33, 21 | lsp0 20886 |
. . . . . . . . . . 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 2831 |
. . . . . . . 8
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π β {(0gβπ)}) |
| 38 | | elsni 4641 |
. . . . . . . 8
β’ (π β
{(0gβπ)}
β π =
(0gβπ)) |
| 39 | 37, 38 | syl 17 |
. . . . . . 7
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π = (0gβπ)) |
| 40 | | lmodgrp 20743 |
. . . . . . . . . 10
β’ (π β LMod β π β Grp) |
| 41 | | grpmnd 18890 |
. . . . . . . . . 10
β’ (π β Grp β π β Mnd) |
| 42 | 20, 40, 41 | 3syl 18 |
. . . . . . . . 9
β’ ((π β LVec β§ π β π) β π β Mnd) |
| 43 | | lbslsat.z |
. . . . . . . . . . 11
β’ 0 =
(0gβπ) |
| 44 | 43, 3, 5 | 0ellsp 33075 |
. . . . . . . . . 10
β’ ((π β LMod β§ {π} β π) β 0 β (πβ{π})) |
| 45 | 1, 2, 44 | syl2an 595 |
. . . . . . . . 9
β’ ((π β LVec β§ π β π) β 0 β (πβ{π})) |
| 46 | 8, 3, 43 | ress0g 18715 |
. . . . . . . . 9
β’ ((π β Mnd β§ 0 β (πβ{π}) β§ (πβ{π}) β π) β 0 =
(0gβπ)) |
| 47 | 42, 45, 15, 46 | syl3anc 1369 |
. . . . . . . 8
β’ ((π β LVec β§ π β π) β 0 =
(0gβπ)) |
| 48 | 47 | adantr 480 |
. . . . . . 7
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β 0 =
(0gβπ)) |
| 49 | 39, 48 | eqtr4d 2771 |
. . . . . 6
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π = 0 ) |
| 50 | 49 | ex 412 |
. . . . 5
β’ ((π β LVec β§ π β π) β (π β ((LSpanβπ)β({π} β {π})) β π = 0 )) |
| 51 | 50 | necon3ad 2949 |
. . . 4
β’ ((π β LVec β§ π β π) β (π β 0 β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
| 52 | 51 | 3impia 1115 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β Β¬ π β ((LSpanβπ)β({π} β {π}))) |
| 53 | | id 22 |
. . . . . . 7
β’ (π₯ = π β π₯ = π) |
| 54 | | sneq 4634 |
. . . . . . . . 9
β’ (π₯ = π β {π₯} = {π}) |
| 55 | 54 | difeq2d 4118 |
. . . . . . . 8
β’ (π₯ = π β ({π} β {π₯}) = ({π} β {π})) |
| 56 | 55 | fveq2d 6895 |
. . . . . . 7
β’ (π₯ = π β ((LSpanβπ)β({π} β {π₯})) = ((LSpanβπ)β({π} β {π}))) |
| 57 | 53, 56 | eleq12d 2823 |
. . . . . 6
β’ (π₯ = π β (π₯ β ((LSpanβπ)β({π} β {π₯})) β π β ((LSpanβπ)β({π} β {π})))) |
| 58 | 57 | notbid 318 |
. . . . 5
β’ (π₯ = π β (Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
| 59 | 58 | ralsng 4673 |
. . . 4
β’ (π β π β (βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
| 60 | 59 | 3ad2ant2 1132 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β (βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
| 61 | 52, 60 | mpbird 257 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯}))) |
| 62 | | eqid 2728 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
| 63 | | eqid 2728 |
. . . 4
β’
(LBasisβπ) =
(LBasisβπ) |
| 64 | 62, 63, 21 | islbs2 21035 |
. . 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 1370 |
1
β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (LBasisβπ)) |
