Step | Hyp | Ref
| Expression |
1 | | lsmelval2.w |
. . . . . 6
β’ (π β π β LMod) |
2 | | lsmelval2.t |
. . . . . 6
β’ (π β π β π) |
3 | | lsmelval2.s |
. . . . . . 7
β’ π = (LSubSpβπ) |
4 | 3 | lsssubg 20433 |
. . . . . 6
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
5 | 1, 2, 4 | syl2anc 585 |
. . . . 5
β’ (π β π β (SubGrpβπ)) |
6 | | lsmelval2.u |
. . . . . 6
β’ (π β π β π) |
7 | 3 | lsssubg 20433 |
. . . . . 6
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
8 | 1, 6, 7 | syl2anc 585 |
. . . . 5
β’ (π β π β (SubGrpβπ)) |
9 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
10 | | lsmelval2.p |
. . . . . 6
β’ β =
(LSSumβπ) |
11 | 9, 10 | lsmelval 19436 |
. . . . 5
β’ ((π β (SubGrpβπ) β§ π β (SubGrpβπ)) β (π β (π β π) β βπ¦ β π βπ§ β π π = (π¦(+gβπ)π§))) |
12 | 5, 8, 11 | syl2anc 585 |
. . . 4
β’ (π β (π β (π β π) β βπ¦ β π βπ§ β π π = (π¦(+gβπ)π§))) |
13 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ π§ β π)) β π β LMod) |
14 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ π§ β π)) β π β π) |
15 | | simprl 770 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ π§ β π)) β π¦ β π) |
16 | | lsmelval2.v |
. . . . . . . . . . . 12
β’ π = (Baseβπ) |
17 | 16, 3 | lssel 20413 |
. . . . . . . . . . 11
β’ ((π β π β§ π¦ β π) β π¦ β π) |
18 | 14, 15, 17 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ π§ β π)) β π¦ β π) |
19 | | lsmelval2.n |
. . . . . . . . . . 11
β’ π = (LSpanβπ) |
20 | 16, 3, 19 | lspsncl 20453 |
. . . . . . . . . 10
β’ ((π β LMod β§ π¦ β π) β (πβ{π¦}) β π) |
21 | 13, 18, 20 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ π§ β π)) β (πβ{π¦}) β π) |
22 | 3 | lsssubg 20433 |
. . . . . . . . 9
β’ ((π β LMod β§ (πβ{π¦}) β π) β (πβ{π¦}) β (SubGrpβπ)) |
23 | 13, 21, 22 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β (πβ{π¦}) β (SubGrpβπ)) |
24 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ π§ β π)) β π β π) |
25 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ π§ β π)) β π§ β π) |
26 | 16, 3 | lssel 20413 |
. . . . . . . . . . 11
β’ ((π β π β§ π§ β π) β π§ β π) |
27 | 24, 25, 26 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ π§ β π)) β π§ β π) |
28 | 16, 3, 19 | lspsncl 20453 |
. . . . . . . . . 10
β’ ((π β LMod β§ π§ β π) β (πβ{π§}) β π) |
29 | 13, 27, 28 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ π§ β π)) β (πβ{π§}) β π) |
30 | 3 | lsssubg 20433 |
. . . . . . . . 9
β’ ((π β LMod β§ (πβ{π§}) β π) β (πβ{π§}) β (SubGrpβπ)) |
31 | 13, 29, 30 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β (πβ{π§}) β (SubGrpβπ)) |
32 | 16, 19 | lspsnid 20469 |
. . . . . . . . 9
β’ ((π β LMod β§ π¦ β π) β π¦ β (πβ{π¦})) |
33 | 13, 18, 32 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β π¦ β (πβ{π¦})) |
34 | 16, 19 | lspsnid 20469 |
. . . . . . . . 9
β’ ((π β LMod β§ π§ β π) β π§ β (πβ{π§})) |
35 | 13, 27, 34 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β π§ β (πβ{π§})) |
36 | 9, 10 | lsmelvali 19437 |
. . . . . . . 8
β’ ((((πβ{π¦}) β (SubGrpβπ) β§ (πβ{π§}) β (SubGrpβπ)) β§ (π¦ β (πβ{π¦}) β§ π§ β (πβ{π§}))) β (π¦(+gβπ)π§) β ((πβ{π¦}) β (πβ{π§}))) |
37 | 23, 31, 33, 35, 36 | syl22anc 838 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β π)) β (π¦(+gβπ)π§) β ((πβ{π¦}) β (πβ{π§}))) |
38 | | eleq1a 2829 |
. . . . . . 7
β’ ((π¦(+gβπ)π§) β ((πβ{π¦}) β (πβ{π§})) β (π = (π¦(+gβπ)π§) β π β ((πβ{π¦}) β (πβ{π§})))) |
39 | 37, 38 | syl 17 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ π§ β π)) β (π = (π¦(+gβπ)π§) β π β ((πβ{π¦}) β (πβ{π§})))) |
40 | 3, 10 | lsmcl 20559 |
. . . . . . . 8
β’ ((π β LMod β§ (πβ{π¦}) β π β§ (πβ{π§}) β π) β ((πβ{π¦}) β (πβ{π§})) β π) |
41 | 13, 21, 29, 40 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β π)) β ((πβ{π¦}) β (πβ{π§})) β π) |
42 | 16, 3, 19, 13, 41 | lspsnel6 20470 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ π§ β π)) β (π β ((πβ{π¦}) β (πβ{π§})) β (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))))) |
43 | 39, 42 | sylibd 238 |
. . . . 5
β’ ((π β§ (π¦ β π β§ π§ β π)) β (π = (π¦(+gβπ)π§) β (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))))) |
44 | 43 | reximdvva 3199 |
. . . 4
β’ (π β (βπ¦ β π βπ§ β π π = (π¦(+gβπ)π§) β βπ¦ β π βπ§ β π (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))))) |
45 | 12, 44 | sylbid 239 |
. . 3
β’ (π β (π β (π β π) β βπ¦ β π βπ§ β π (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))))) |
46 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β π β (SubGrpβπ)) |
47 | 3, 19, 13, 14, 15 | lspsnel5a 20472 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β (πβ{π¦}) β π) |
48 | 10 | lsmless1 19447 |
. . . . . . . 8
β’ ((π β (SubGrpβπ) β§ (πβ{π§}) β (SubGrpβπ) β§ (πβ{π¦}) β π) β ((πβ{π¦}) β (πβ{π§})) β (π β (πβ{π§}))) |
49 | 46, 31, 47, 48 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β π)) β ((πβ{π¦}) β (πβ{π§})) β (π β (πβ{π§}))) |
50 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β π β (SubGrpβπ)) |
51 | 3, 19, 13, 24, 25 | lspsnel5a 20472 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β (πβ{π§}) β π) |
52 | 10 | lsmless2 19448 |
. . . . . . . 8
β’ ((π β (SubGrpβπ) β§ π β (SubGrpβπ) β§ (πβ{π§}) β π) β (π β (πβ{π§})) β (π β π)) |
53 | 46, 50, 51, 52 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β π)) β (π β (πβ{π§})) β (π β π)) |
54 | 49, 53 | sstrd 3955 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ π§ β π)) β ((πβ{π¦}) β (πβ{π§})) β (π β π)) |
55 | 54 | sseld 3944 |
. . . . 5
β’ ((π β§ (π¦ β π β§ π§ β π)) β (π β ((πβ{π¦}) β (πβ{π§})) β π β (π β π))) |
56 | 42, 55 | sylbird 260 |
. . . 4
β’ ((π β§ (π¦ β π β§ π§ β π)) β ((π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))) β π β (π β π))) |
57 | 56 | rexlimdvva 3202 |
. . 3
β’ (π β (βπ¦ β π βπ§ β π (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))) β π β (π β π))) |
58 | 45, 57 | impbid 211 |
. 2
β’ (π β (π β (π β π) β βπ¦ β π βπ§ β π (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))))) |
59 | | r19.42v 3184 |
. . . 4
β’
(βπ§ β
π (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))) β (π β π β§ βπ§ β π (πβ{π}) β ((πβ{π¦}) β (πβ{π§})))) |
60 | 59 | rexbii 3094 |
. . 3
β’
(βπ¦ β
π βπ§ β π (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))) β βπ¦ β π (π β π β§ βπ§ β π (πβ{π}) β ((πβ{π¦}) β (πβ{π§})))) |
61 | | r19.42v 3184 |
. . 3
β’
(βπ¦ β
π (π β π β§ βπ§ β π (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))) β (π β π β§ βπ¦ β π βπ§ β π (πβ{π}) β ((πβ{π¦}) β (πβ{π§})))) |
62 | 60, 61 | bitri 275 |
. 2
β’
(βπ¦ β
π βπ§ β π (π β π β§ (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))) β (π β π β§ βπ¦ β π βπ§ β π (πβ{π}) β ((πβ{π¦}) β (πβ{π§})))) |
63 | 58, 62 | bitrdi 287 |
1
β’ (π β (π β (π β π) β (π β π β§ βπ¦ β π βπ§ β π (πβ{π}) β ((πβ{π¦}) β (πβ{π§}))))) |