Step | Hyp | Ref
| Expression |
1 | | lspprabs.w |
. . . . . . 7
β’ (π β π β LMod) |
2 | | eqid 2737 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
3 | 2 | lsssssubg 20435 |
. . . . . . 7
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
4 | 1, 3 | syl 17 |
. . . . . 6
β’ (π β (LSubSpβπ) β (SubGrpβπ)) |
5 | | lspprabs.x |
. . . . . . 7
β’ (π β π β π) |
6 | | lspprabs.v |
. . . . . . . 8
β’ π = (Baseβπ) |
7 | | lspprabs.n |
. . . . . . . 8
β’ π = (LSpanβπ) |
8 | 6, 2, 7 | lspsncl 20454 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
9 | 1, 5, 8 | syl2anc 585 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
10 | 4, 9 | sseldd 3950 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
11 | | lspprabs.y |
. . . . . . 7
β’ (π β π β π) |
12 | 6, 2, 7 | lspsncl 20454 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
13 | 1, 11, 12 | syl2anc 585 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
14 | 4, 13 | sseldd 3950 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
15 | | eqid 2737 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
16 | 15 | lsmub1 19446 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
17 | 10, 14, 16 | syl2anc 585 |
. . . 4
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
18 | 2, 15 | lsmcl 20560 |
. . . . . 6
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
19 | 1, 9, 13, 18 | syl3anc 1372 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
20 | 6, 7 | lspsnid 20470 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
21 | 1, 5, 20 | syl2anc 585 |
. . . . . 6
β’ (π β π β (πβ{π})) |
22 | 6, 7 | lspsnid 20470 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
23 | 1, 11, 22 | syl2anc 585 |
. . . . . 6
β’ (π β π β (πβ{π})) |
24 | | lspprabs.p |
. . . . . . 7
β’ + =
(+gβπ) |
25 | 24, 15 | lsmelvali 19439 |
. . . . . 6
β’ ((((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β§ (π β (πβ{π}) β§ π β (πβ{π}))) β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
26 | 10, 14, 21, 23, 25 | syl22anc 838 |
. . . . 5
β’ (π β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
27 | 2, 7, 1, 19, 26 | lspsnel5a 20473 |
. . . 4
β’ (π β (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
28 | 6, 24 | lmodvacl 20352 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
29 | 1, 5, 11, 28 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π + π) β π) |
30 | 6, 2, 7 | lspsncl 20454 |
. . . . . . 7
β’ ((π β LMod β§ (π + π) β π) β (πβ{(π + π)}) β (LSubSpβπ)) |
31 | 1, 29, 30 | syl2anc 585 |
. . . . . 6
β’ (π β (πβ{(π + π)}) β (LSubSpβπ)) |
32 | 4, 31 | sseldd 3950 |
. . . . 5
β’ (π β (πβ{(π + π)}) β (SubGrpβπ)) |
33 | 4, 19 | sseldd 3950 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (SubGrpβπ)) |
34 | 15 | lsmlub 19453 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{(π + π)}) β (SubGrpβπ) β§ ((πβ{π})(LSSumβπ)(πβ{π})) β (SubGrpβπ)) β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π})) β§ (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β ((πβ{π})(LSSumβπ)(πβ{π})))) |
35 | 10, 32, 33, 34 | syl3anc 1372 |
. . . 4
β’ (π β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π})) β§ (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β ((πβ{π})(LSSumβπ)(πβ{π})))) |
36 | 17, 27, 35 | mpbi2and 711 |
. . 3
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
37 | 15 | lsmub1 19446 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{(π + π)}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
38 | 10, 32, 37 | syl2anc 585 |
. . . 4
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
39 | 2, 15 | lsmcl 20560 |
. . . . . 6
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{(π + π)}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (LSubSpβπ)) |
40 | 1, 9, 31, 39 | syl3anc 1372 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (LSubSpβπ)) |
41 | | eqid 2737 |
. . . . . . 7
β’
(-gβπ) = (-gβπ) |
42 | 6, 7 | lspsnid 20470 |
. . . . . . . 8
β’ ((π β LMod β§ (π + π) β π) β (π + π) β (πβ{(π + π)})) |
43 | 1, 29, 42 | syl2anc 585 |
. . . . . . 7
β’ (π β (π + π) β (πβ{(π + π)})) |
44 | 41, 15, 32, 10, 43, 21 | lsmelvalmi 19441 |
. . . . . 6
β’ (π β ((π + π)(-gβπ)π) β ((πβ{(π + π)})(LSSumβπ)(πβ{π}))) |
45 | | lmodabl 20385 |
. . . . . . . 8
β’ (π β LMod β π β Abel) |
46 | 1, 45 | syl 17 |
. . . . . . 7
β’ (π β π β Abel) |
47 | 6, 24, 41 | ablpncan2 19601 |
. . . . . . 7
β’ ((π β Abel β§ π β π β§ π β π) β ((π + π)(-gβπ)π) = π) |
48 | 46, 5, 11, 47 | syl3anc 1372 |
. . . . . 6
β’ (π β ((π + π)(-gβπ)π) = π) |
49 | 15 | lsmcom 19643 |
. . . . . . 7
β’ ((π β Abel β§ (πβ{(π + π)}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β ((πβ{(π + π)})(LSSumβπ)(πβ{π})) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
50 | 46, 32, 10, 49 | syl3anc 1372 |
. . . . . 6
β’ (π β ((πβ{(π + π)})(LSSumβπ)(πβ{π})) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
51 | 44, 48, 50 | 3eltr3d 2852 |
. . . . 5
β’ (π β π β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
52 | 2, 7, 1, 40, 51 | lspsnel5a 20473 |
. . . 4
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
53 | 4, 40 | sseldd 3950 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (SubGrpβπ)) |
54 | 15 | lsmlub 19453 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ) β§ ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (SubGrpβπ)) β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β§ (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) β ((πβ{π})(LSSumβπ)(πβ{π})) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})))) |
55 | 10, 14, 53, 54 | syl3anc 1372 |
. . . 4
β’ (π β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β§ (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) β ((πβ{π})(LSSumβπ)(πβ{π})) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})))) |
56 | 38, 52, 55 | mpbi2and 711 |
. . 3
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
57 | 36, 56 | eqssd 3966 |
. 2
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
58 | 6, 7, 15, 1, 5, 29 | lsmpr 20566 |
. 2
β’ (π β (πβ{π, (π + π)}) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
59 | 6, 7, 15, 1, 5, 11 | lsmpr 20566 |
. 2
β’ (π β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
60 | 57, 58, 59 | 3eqtr4d 2787 |
1
β’ (π β (πβ{π, (π + π)}) = (πβ{π, π})) |