Step | Hyp | Ref
| Expression |
1 | | eleq1 2826 |
. . . . 5
β’ (π¦ = (0gβπ) β (π¦ β (πββͺ {π₯ β π΄ β£ π₯ β π}) β (0gβπ) β (πββͺ {π₯ β π΄ β£ π₯ β π}))) |
2 | | simplll 774 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β π β LMod) |
3 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β π β π) |
4 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β π¦ β π) |
5 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
6 | | lssats.s |
. . . . . . . . . . 11
β’ π = (LSubSpβπ) |
7 | 5, 6 | lssel 20414 |
. . . . . . . . . 10
β’ ((π β π β§ π¦ β π) β π¦ β (Baseβπ)) |
8 | 3, 4, 7 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β π¦ β (Baseβπ)) |
9 | | lssats.n |
. . . . . . . . . 10
β’ π = (LSpanβπ) |
10 | 5, 6, 9 | lspsncl 20454 |
. . . . . . . . 9
β’ ((π β LMod β§ π¦ β (Baseβπ)) β (πβ{π¦}) β π) |
11 | 2, 8, 10 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ{π¦}) β π) |
12 | 6, 9 | lspid 20459 |
. . . . . . . 8
β’ ((π β LMod β§ (πβ{π¦}) β π) β (πβ(πβ{π¦})) = (πβ{π¦})) |
13 | 2, 11, 12 | syl2anc 585 |
. . . . . . 7
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ(πβ{π¦})) = (πβ{π¦})) |
14 | | lssats.a |
. . . . . . . . . . . . 13
β’ π΄ = (LSAtomsβπ) |
15 | 6, 14 | lsatlss 37487 |
. . . . . . . . . . . 12
β’ (π β LMod β π΄ β π) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π) β π΄ β π) |
17 | | rabss2 4040 |
. . . . . . . . . . 11
β’ (π΄ β π β {π₯ β π΄ β£ π₯ β π} β {π₯ β π β£ π₯ β π}) |
18 | | uniss 4878 |
. . . . . . . . . . 11
β’ ({π₯ β π΄ β£ π₯ β π} β {π₯ β π β£ π₯ β π} β βͺ {π₯ β π΄ β£ π₯ β π} β βͺ
{π₯ β π β£ π₯ β π}) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β βͺ {π₯ β π΄ β£ π₯ β π} β βͺ
{π₯ β π β£ π₯ β π}) |
20 | | unimax 4910 |
. . . . . . . . . . . 12
β’ (π β π β βͺ {π₯ β π β£ π₯ β π} = π) |
21 | 5, 6 | lssss 20413 |
. . . . . . . . . . . 12
β’ (π β π β π β (Baseβπ)) |
22 | 20, 21 | eqsstrd 3987 |
. . . . . . . . . . 11
β’ (π β π β βͺ {π₯ β π β£ π₯ β π} β (Baseβπ)) |
23 | 22 | adantl 483 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β βͺ {π₯ β π β£ π₯ β π} β (Baseβπ)) |
24 | 19, 23 | sstrd 3959 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π) β βͺ {π₯ β π΄ β£ π₯ β π} β (Baseβπ)) |
25 | 24 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β βͺ
{π₯ β π΄ β£ π₯ β π} β (Baseβπ)) |
26 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β π¦ β (0gβπ)) |
27 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
28 | 5, 9, 27, 14 | lsatlspsn2 37483 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π¦ β (Baseβπ) β§ π¦ β (0gβπ)) β (πβ{π¦}) β π΄) |
29 | 2, 8, 26, 28 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ{π¦}) β π΄) |
30 | 6, 9, 2, 3, 4 | lspsnel5a 20473 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ{π¦}) β π) |
31 | | sseq1 3974 |
. . . . . . . . . . 11
β’ (π₯ = (πβ{π¦}) β (π₯ β π β (πβ{π¦}) β π)) |
32 | 31 | elrab 3650 |
. . . . . . . . . 10
β’ ((πβ{π¦}) β {π₯ β π΄ β£ π₯ β π} β ((πβ{π¦}) β π΄ β§ (πβ{π¦}) β π)) |
33 | 29, 30, 32 | sylanbrc 584 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ{π¦}) β {π₯ β π΄ β£ π₯ β π}) |
34 | | elssuni 4903 |
. . . . . . . . 9
β’ ((πβ{π¦}) β {π₯ β π΄ β£ π₯ β π} β (πβ{π¦}) β βͺ
{π₯ β π΄ β£ π₯ β π}) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ{π¦}) β βͺ
{π₯ β π΄ β£ π₯ β π}) |
36 | 5, 9 | lspss 20461 |
. . . . . . . 8
β’ ((π β LMod β§ βͺ {π₯
β π΄ β£ π₯ β π} β (Baseβπ) β§ (πβ{π¦}) β βͺ
{π₯ β π΄ β£ π₯ β π}) β (πβ(πβ{π¦})) β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
37 | 2, 25, 35, 36 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ(πβ{π¦})) β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
38 | 13, 37 | eqsstrrd 3988 |
. . . . . 6
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β (πβ{π¦}) β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
39 | 5, 9 | lspsnid 20470 |
. . . . . . 7
β’ ((π β LMod β§ π¦ β (Baseβπ)) β π¦ β (πβ{π¦})) |
40 | 2, 8, 39 | syl2anc 585 |
. . . . . 6
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β π¦ β (πβ{π¦})) |
41 | 38, 40 | sseldd 3950 |
. . . . 5
β’ ((((π β LMod β§ π β π) β§ π¦ β π) β§ π¦ β (0gβπ)) β π¦ β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
42 | | simpll 766 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ π¦ β π) β π β LMod) |
43 | 5, 6, 9 | lspcl 20453 |
. . . . . . . 8
β’ ((π β LMod β§ βͺ {π₯
β π΄ β£ π₯ β π} β (Baseβπ)) β (πββͺ {π₯ β π΄ β£ π₯ β π}) β π) |
44 | 24, 43 | syldan 592 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πββͺ {π₯ β π΄ β£ π₯ β π}) β π) |
45 | 44 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ π¦ β π) β (πββͺ {π₯ β π΄ β£ π₯ β π}) β π) |
46 | 27, 6 | lss0cl 20423 |
. . . . . 6
β’ ((π β LMod β§ (πββͺ {π₯
β π΄ β£ π₯ β π}) β π) β (0gβπ) β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
47 | 42, 45, 46 | syl2anc 585 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ π¦ β π) β (0gβπ) β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
48 | 1, 41, 47 | pm2.61ne 3031 |
. . . 4
β’ (((π β LMod β§ π β π) β§ π¦ β π) β π¦ β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
49 | 48 | ex 414 |
. . 3
β’ ((π β LMod β§ π β π) β (π¦ β π β π¦ β (πββͺ {π₯ β π΄ β£ π₯ β π}))) |
50 | 49 | ssrdv 3955 |
. 2
β’ ((π β LMod β§ π β π) β π β (πββͺ {π₯ β π΄ β£ π₯ β π})) |
51 | | simpl 484 |
. . . 4
β’ ((π β LMod β§ π β π) β π β LMod) |
52 | 5, 9 | lspss 20461 |
. . . 4
β’ ((π β LMod β§ βͺ {π₯
β π β£ π₯ β π} β (Baseβπ) β§ βͺ {π₯ β π΄ β£ π₯ β π} β βͺ
{π₯ β π β£ π₯ β π}) β (πββͺ {π₯ β π΄ β£ π₯ β π}) β (πββͺ {π₯ β π β£ π₯ β π})) |
53 | 51, 23, 19, 52 | syl3anc 1372 |
. . 3
β’ ((π β LMod β§ π β π) β (πββͺ {π₯ β π΄ β£ π₯ β π}) β (πββͺ {π₯ β π β£ π₯ β π})) |
54 | 20 | adantl 483 |
. . . . 5
β’ ((π β LMod β§ π β π) β βͺ {π₯ β π β£ π₯ β π} = π) |
55 | 54 | fveq2d 6851 |
. . . 4
β’ ((π β LMod β§ π β π) β (πββͺ {π₯ β π β£ π₯ β π}) = (πβπ)) |
56 | 6, 9 | lspid 20459 |
. . . 4
β’ ((π β LMod β§ π β π) β (πβπ) = π) |
57 | 55, 56 | eqtrd 2777 |
. . 3
β’ ((π β LMod β§ π β π) β (πββͺ {π₯ β π β£ π₯ β π}) = π) |
58 | 53, 57 | sseqtrd 3989 |
. 2
β’ ((π β LMod β§ π β π) β (πββͺ {π₯ β π΄ β£ π₯ β π}) β π) |
59 | 50, 58 | eqssd 3966 |
1
β’ ((π β LMod β§ π β π) β π = (πββͺ {π₯ β π΄ β£ π₯ β π})) |