Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
2 | | mapdindp1.n |
. . . 4
β’ π = (LSpanβπ) |
3 | | mapdindp1.w |
. . . . 5
β’ (π β π β LVec) |
4 | | lveclmod 20582 |
. . . . 5
β’ (π β LVec β π β LMod) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β π β LMod) |
6 | | mapdindp1.y |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
7 | 6 | eldifad 3923 |
. . . . . 6
β’ (π β π β π) |
8 | | mapdindp1.v |
. . . . . . 7
β’ π = (Baseβπ) |
9 | 8, 1, 2 | lspsncl 20453 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
10 | 5, 7, 9 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
11 | | mapdindp1.e |
. . . . . 6
β’ (π β (πβ{π}) = (πβ{π})) |
12 | 11, 10 | eqeltrrd 2835 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
13 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
14 | 1, 13 | lsmcl 20559 |
. . . . 5
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
15 | 5, 10, 12, 14 | syl3anc 1372 |
. . . 4
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
16 | 1 | lsssssubg 20434 |
. . . . . . 7
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
17 | 5, 16 | syl 17 |
. . . . . 6
β’ (π β (LSubSpβπ) β (SubGrpβπ)) |
18 | 17, 10 | sseldd 3946 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
19 | 11, 18 | eqeltrrd 2835 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
20 | 8, 2 | lspsnid 20469 |
. . . . . 6
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
21 | 5, 7, 20 | syl2anc 585 |
. . . . 5
β’ (π β π β (πβ{π})) |
22 | | mapdindp1.z |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
23 | 22 | eldifad 3923 |
. . . . . 6
β’ (π β π β π) |
24 | 8, 2 | lspsnid 20469 |
. . . . . 6
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
25 | 5, 23, 24 | syl2anc 585 |
. . . . 5
β’ (π β π β (πβ{π})) |
26 | | mapdindp1.p |
. . . . . 6
β’ + =
(+gβπ) |
27 | 26, 13 | lsmelvali 19437 |
. . . . 5
β’ ((((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β§ (π β (πβ{π}) β§ π β (πβ{π}))) β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
28 | 18, 19, 21, 25, 27 | syl22anc 838 |
. . . 4
β’ (π β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
29 | 1, 2, 5, 15, 28 | lspsnel5a 20472 |
. . 3
β’ (π β (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
30 | 11 | oveq2d 7374 |
. . . 4
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
31 | 13 | lsmidm 19450 |
. . . . 5
β’ ((πβ{π}) β (SubGrpβπ) β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
32 | 18, 31 | syl 17 |
. . . 4
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
33 | 30, 32 | eqtr3d 2775 |
. . 3
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
34 | 29, 33 | sseqtrd 3985 |
. 2
β’ (π β (πβ{(π + π)}) β (πβ{π})) |
35 | | mapdindp1.o |
. . 3
β’ 0 =
(0gβπ) |
36 | 8, 26 | lmodvacl 20351 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
37 | 5, 7, 23, 36 | syl3anc 1372 |
. . . 4
β’ (π β (π + π) β π) |
38 | | mapdindp1.yz |
. . . 4
β’ (π β (π + π) β 0 ) |
39 | | eldifsn 4748 |
. . . 4
β’ ((π + π) β (π β { 0 }) β ((π + π) β π β§ (π + π) β 0 )) |
40 | 37, 38, 39 | sylanbrc 584 |
. . 3
β’ (π β (π + π) β (π β { 0 })) |
41 | 8, 35, 2, 3, 40, 7 | lspsncmp 20593 |
. 2
β’ (π β ((πβ{(π + π)}) β (πβ{π}) β (πβ{(π + π)}) = (πβ{π}))) |
42 | 34, 41 | mpbid 231 |
1
β’ (π β (πβ{(π + π)}) = (πβ{π})) |