| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lspprabs.w |
. . . . . . 7
β’ (π β π β LMod) |
| 2 | | eqid 2728 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 3 | 2 | lsssssubg 20856 |
. . . . . . 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 20875 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 9 | 1, 5, 8 | syl2anc 582 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
| 10 | 4, 9 | sseldd 3983 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
| 11 | | lspprabs.y |
. . . . . . 7
β’ (π β π β π) |
| 12 | 6, 2, 7 | lspsncl 20875 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 13 | 1, 11, 12 | syl2anc 582 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
| 14 | 4, 13 | sseldd 3983 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
| 15 | | eqid 2728 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
| 16 | 15 | lsmub1 19626 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 17 | 10, 14, 16 | syl2anc 582 |
. . . 4
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 18 | 2, 15 | lsmcl 20982 |
. . . . . 6
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
| 19 | 1, 9, 13, 18 | syl3anc 1368 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
| 20 | 6, 7 | lspsnid 20891 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
| 21 | 1, 5, 20 | syl2anc 582 |
. . . . . 6
β’ (π β π β (πβ{π})) |
| 22 | 6, 7 | lspsnid 20891 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
| 23 | 1, 11, 22 | syl2anc 582 |
. . . . . 6
β’ (π β π β (πβ{π})) |
| 24 | | lspprabs.p |
. . . . . . 7
β’ + =
(+gβπ) |
| 25 | 24, 15 | lsmelvali 19619 |
. . . . . 6
β’ ((((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β§ (π β (πβ{π}) β§ π β (πβ{π}))) β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 26 | 10, 14, 21, 23, 25 | syl22anc 837 |
. . . . 5
β’ (π β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 27 | 2, 7, 1, 19, 26 | lspsnel5a 20894 |
. . . 4
β’ (π β (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 28 | 6, 24 | lmodvacl 20772 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
| 29 | 1, 5, 11, 28 | syl3anc 1368 |
. . . . . . 7
β’ (π β (π + π) β π) |
| 30 | 6, 2, 7 | lspsncl 20875 |
. . . . . . 7
β’ ((π β LMod β§ (π + π) β π) β (πβ{(π + π)}) β (LSubSpβπ)) |
| 31 | 1, 29, 30 | syl2anc 582 |
. . . . . 6
β’ (π β (πβ{(π + π)}) β (LSubSpβπ)) |
| 32 | 4, 31 | sseldd 3983 |
. . . . 5
β’ (π β (πβ{(π + π)}) β (SubGrpβπ)) |
| 33 | 4, 19 | sseldd 3983 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (SubGrpβπ)) |
| 34 | 15 | lsmlub 19633 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{(π + π)}) β (SubGrpβπ) β§ ((πβ{π})(LSSumβπ)(πβ{π})) β (SubGrpβπ)) β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π})) β§ (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β ((πβ{π})(LSSumβπ)(πβ{π})))) |
| 35 | 10, 32, 33, 34 | syl3anc 1368 |
. . . 4
β’ (π β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π})) β§ (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β ((πβ{π})(LSSumβπ)(πβ{π})))) |
| 36 | 17, 27, 35 | mpbi2and 710 |
. . 3
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 37 | 15 | lsmub1 19626 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{(π + π)}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 38 | 10, 32, 37 | syl2anc 582 |
. . . 4
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 39 | 2, 15 | lsmcl 20982 |
. . . . . 6
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{(π + π)}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (LSubSpβπ)) |
| 40 | 1, 9, 31, 39 | syl3anc 1368 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (LSubSpβπ)) |
| 41 | | eqid 2728 |
. . . . . . 7
β’
(-gβπ) = (-gβπ) |
| 42 | 6, 7 | lspsnid 20891 |
. . . . . . . 8
β’ ((π β LMod β§ (π + π) β π) β (π + π) β (πβ{(π + π)})) |
| 43 | 1, 29, 42 | syl2anc 582 |
. . . . . . 7
β’ (π β (π + π) β (πβ{(π + π)})) |
| 44 | 41, 15, 32, 10, 43, 21 | lsmelvalmi 19621 |
. . . . . 6
β’ (π β ((π + π)(-gβπ)π) β ((πβ{(π + π)})(LSSumβπ)(πβ{π}))) |
| 45 | | lmodabl 20806 |
. . . . . . . 8
β’ (π β LMod β π β Abel) |
| 46 | 1, 45 | syl 17 |
. . . . . . 7
β’ (π β π β Abel) |
| 47 | 6, 24, 41 | ablpncan2 19784 |
. . . . . . 7
β’ ((π β Abel β§ π β π β§ π β π) β ((π + π)(-gβπ)π) = π) |
| 48 | 46, 5, 11, 47 | syl3anc 1368 |
. . . . . 6
β’ (π β ((π + π)(-gβπ)π) = π) |
| 49 | 15 | lsmcom 19827 |
. . . . . . 7
β’ ((π β Abel β§ (πβ{(π + π)}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β ((πβ{(π + π)})(LSSumβπ)(πβ{π})) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 50 | 46, 32, 10, 49 | syl3anc 1368 |
. . . . . 6
β’ (π β ((πβ{(π + π)})(LSSumβπ)(πβ{π})) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 51 | 44, 48, 50 | 3eltr3d 2843 |
. . . . 5
β’ (π β π β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 52 | 2, 7, 1, 40, 51 | lspsnel5a 20894 |
. . . 4
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 53 | 4, 40 | sseldd 3983 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (SubGrpβπ)) |
| 54 | 15 | lsmlub 19633 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ) β§ ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β (SubGrpβπ)) β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β§ (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) β ((πβ{π})(LSSumβπ)(πβ{π})) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})))) |
| 55 | 10, 14, 53, 54 | syl3anc 1368 |
. . . 4
β’ (π β (((πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) β§ (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) β ((πβ{π})(LSSumβπ)(πβ{π})) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})))) |
| 56 | 38, 52, 55 | mpbi2and 710 |
. . 3
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 57 | 36, 56 | eqssd 3999 |
. 2
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 58 | 6, 7, 15, 1, 5, 29 | lsmpr 20988 |
. 2
β’ (π β (πβ{π, (π + π)}) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
| 59 | 6, 7, 15, 1, 5, 11 | lsmpr 20988 |
. 2
β’ (π β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 60 | 57, 58, 59 | 3eqtr4d 2778 |
1
β’ (π β (πβ{π, (π + π)}) = (πβ{π, π})) |
