Step | Hyp | Ref
| Expression |
1 | | lveclmod 20611 |
. . . . . 6
β’ (π β LVec β π β LMod) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β LVec β§ π β π) β π β LMod) |
3 | | snssi 4772 |
. . . . . 6
β’ (π β π β {π} β π) |
4 | 3 | adantl 483 |
. . . . 5
β’ ((π β LVec β§ π β π) β {π} β π) |
5 | | lbslsat.v |
. . . . . 6
β’ π = (Baseβπ) |
6 | | eqid 2733 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
7 | | lbslsat.n |
. . . . . 6
β’ π = (LSpanβπ) |
8 | 5, 6, 7 | lspcl 20481 |
. . . . 5
β’ ((π β LMod β§ {π} β π) β (πβ{π}) β (LSubSpβπ)) |
9 | 2, 4, 8 | syl2anc 585 |
. . . 4
β’ ((π β LVec β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
10 | | lbslsat.y |
. . . . 5
β’ π = (π βΎs (πβ{π})) |
11 | 10, 6 | lsslvec 20613 |
. . . 4
β’ ((π β LVec β§ (πβ{π}) β (LSubSpβπ)) β π β LVec) |
12 | 9, 11 | syldan 592 |
. . 3
β’ ((π β LVec β§ π β π) β π β LVec) |
13 | 12 | 3adant3 1133 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β π β LVec) |
14 | 5, 7 | lspssid 20490 |
. . . . 5
β’ ((π β LMod β§ {π} β π) β {π} β (πβ{π})) |
15 | 2, 4, 14 | syl2anc 585 |
. . . 4
β’ ((π β LVec β§ π β π) β {π} β (πβ{π})) |
16 | 5, 7 | lspssv 20488 |
. . . . . 6
β’ ((π β LMod β§ {π} β π) β (πβ{π}) β π) |
17 | 2, 4, 16 | syl2anc 585 |
. . . . 5
β’ ((π β LVec β§ π β π) β (πβ{π}) β π) |
18 | 10, 5 | ressbas2 17128 |
. . . . 5
β’ ((πβ{π}) β π β (πβ{π}) = (Baseβπ)) |
19 | 17, 18 | syl 17 |
. . . 4
β’ ((π β LVec β§ π β π) β (πβ{π}) = (Baseβπ)) |
20 | 15, 19 | sseqtrd 3988 |
. . 3
β’ ((π β LVec β§ π β π) β {π} β (Baseβπ)) |
21 | 20 | 3adant3 1133 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (Baseβπ)) |
22 | 2 | 3adant3 1133 |
. . . 4
β’ ((π β LVec β§ π β π β§ π β 0 ) β π β LMod) |
23 | 9 | 3adant3 1133 |
. . . 4
β’ ((π β LVec β§ π β π β§ π β 0 ) β (πβ{π}) β (LSubSpβπ)) |
24 | 15 | 3adant3 1133 |
. . . 4
β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (πβ{π})) |
25 | | eqid 2733 |
. . . . 5
β’
(LSpanβπ) =
(LSpanβπ) |
26 | 10, 7, 25, 6 | lsslsp 20520 |
. . . 4
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ {π} β (πβ{π})) β (πβ{π}) = ((LSpanβπ)β{π})) |
27 | 22, 23, 24, 26 | syl3anc 1372 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β (πβ{π}) = ((LSpanβπ)β{π})) |
28 | 19 | 3adant3 1133 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β (πβ{π}) = (Baseβπ)) |
29 | 27, 28 | eqtr3d 2775 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β
((LSpanβπ)β{π}) = (Baseβπ)) |
30 | | difid 4334 |
. . . . . . . . . . . . 13
β’ ({π} β {π}) = β
|
31 | 30 | fveq2i 6849 |
. . . . . . . . . . . 12
β’
((LSpanβπ)β({π} β {π})) = ((LSpanβπ)ββ
) |
32 | 31 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β LVec β§ π β π) β ((LSpanβπ)β({π} β {π})) = ((LSpanβπ)ββ
)) |
33 | 32 | eleq2d 2820 |
. . . . . . . . . 10
β’ ((π β LVec β§ π β π) β (π β ((LSpanβπ)β({π} β {π})) β π β ((LSpanβπ)ββ
))) |
34 | 33 | biimpa 478 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π β ((LSpanβπ)ββ
)) |
35 | | lveclmod 20611 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
36 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
37 | 36, 25 | lsp0 20514 |
. . . . . . . . . . 11
β’ (π β LMod β
((LSpanβπ)ββ
) =
{(0gβπ)}) |
38 | 12, 35, 37 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β LVec β§ π β π) β ((LSpanβπ)ββ
) =
{(0gβπ)}) |
39 | 38 | adantr 482 |
. . . . . . . . 9
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β ((LSpanβπ)ββ
) =
{(0gβπ)}) |
40 | 34, 39 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π β {(0gβπ)}) |
41 | | elsni 4607 |
. . . . . . . 8
β’ (π β
{(0gβπ)}
β π =
(0gβπ)) |
42 | 40, 41 | syl 17 |
. . . . . . 7
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π = (0gβπ)) |
43 | | lmodgrp 20372 |
. . . . . . . . . 10
β’ (π β LMod β π β Grp) |
44 | | grpmnd 18763 |
. . . . . . . . . 10
β’ (π β Grp β π β Mnd) |
45 | 2, 43, 44 | 3syl 18 |
. . . . . . . . 9
β’ ((π β LVec β§ π β π) β π β Mnd) |
46 | | lbslsat.z |
. . . . . . . . . . 11
β’ 0 =
(0gβπ) |
47 | 46, 5, 7 | 0ellsp 32212 |
. . . . . . . . . 10
β’ ((π β LMod β§ {π} β π) β 0 β (πβ{π})) |
48 | 2, 4, 47 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β LVec β§ π β π) β 0 β (πβ{π})) |
49 | 10, 5, 46 | ress0g 18592 |
. . . . . . . . 9
β’ ((π β Mnd β§ 0 β (πβ{π}) β§ (πβ{π}) β π) β 0 =
(0gβπ)) |
50 | 45, 48, 17, 49 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β LVec β§ π β π) β 0 =
(0gβπ)) |
51 | 50 | adantr 482 |
. . . . . . 7
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β 0 =
(0gβπ)) |
52 | 42, 51 | eqtr4d 2776 |
. . . . . 6
β’ (((π β LVec β§ π β π) β§ π β ((LSpanβπ)β({π} β {π}))) β π = 0 ) |
53 | 52 | ex 414 |
. . . . 5
β’ ((π β LVec β§ π β π) β (π β ((LSpanβπ)β({π} β {π})) β π = 0 )) |
54 | 53 | necon3ad 2953 |
. . . 4
β’ ((π β LVec β§ π β π) β (π β 0 β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
55 | 54 | 3impia 1118 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β Β¬ π β ((LSpanβπ)β({π} β {π}))) |
56 | | id 22 |
. . . . . . 7
β’ (π₯ = π β π₯ = π) |
57 | | sneq 4600 |
. . . . . . . . 9
β’ (π₯ = π β {π₯} = {π}) |
58 | 57 | difeq2d 4086 |
. . . . . . . 8
β’ (π₯ = π β ({π} β {π₯}) = ({π} β {π})) |
59 | 58 | fveq2d 6850 |
. . . . . . 7
β’ (π₯ = π β ((LSpanβπ)β({π} β {π₯})) = ((LSpanβπ)β({π} β {π}))) |
60 | 56, 59 | eleq12d 2828 |
. . . . . 6
β’ (π₯ = π β (π₯ β ((LSpanβπ)β({π} β {π₯})) β π β ((LSpanβπ)β({π} β {π})))) |
61 | 60 | notbid 318 |
. . . . 5
β’ (π₯ = π β (Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
62 | 61 | ralsng 4638 |
. . . 4
β’ (π β π β (βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
63 | 62 | 3ad2ant2 1135 |
. . 3
β’ ((π β LVec β§ π β π β§ π β 0 ) β (βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})) β Β¬ π β ((LSpanβπ)β({π} β {π})))) |
64 | 55, 63 | mpbird 257 |
. 2
β’ ((π β LVec β§ π β π β§ π β 0 ) β βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯}))) |
65 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
66 | | eqid 2733 |
. . . 4
β’
(LBasisβπ) =
(LBasisβπ) |
67 | 65, 66, 25 | islbs2 20660 |
. . 3
β’ (π β LVec β ({π} β (LBasisβπ) β ({π} β (Baseβπ) β§ ((LSpanβπ)β{π}) = (Baseβπ) β§ βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯}))))) |
68 | 67 | biimpar 479 |
. 2
β’ ((π β LVec β§ ({π} β (Baseβπ) β§ ((LSpanβπ)β{π}) = (Baseβπ) β§ βπ₯ β {π} Β¬ π₯ β ((LSpanβπ)β({π} β {π₯})))) β {π} β (LBasisβπ)) |
69 | 13, 21, 29, 64, 68 | syl13anc 1373 |
1
β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (LBasisβπ)) |