| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2726 |
. . . . 5
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 2 | | lspabs2.n |
. . . . 5
β’ π = (LSpanβπ) |
| 3 | | lspabs2.w |
. . . . . 6
β’ (π β π β LVec) |
| 4 | | lveclmod 20951 |
. . . . . 6
β’ (π β LVec β π β LMod) |
| 5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β π β LMod) |
| 6 | | lspabs2.x |
. . . . . . 7
β’ (π β π β π) |
| 7 | | lspabs2.v |
. . . . . . . 8
β’ π = (Baseβπ) |
| 8 | 7, 1, 2 | lspsncl 20821 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 9 | 5, 6, 8 | syl2anc 583 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
| 10 | | lspabs3.y |
. . . . . . 7
β’ (π β π β π) |
| 11 | 7, 1, 2 | lspsncl 20821 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 12 | 5, 10, 11 | syl2anc 583 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
| 13 | | eqid 2726 |
. . . . . . 7
β’
(LSSumβπ) =
(LSSumβπ) |
| 14 | 1, 13 | lsmcl 20928 |
. . . . . 6
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
| 15 | 5, 9, 12, 14 | syl3anc 1368 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
| 16 | 7, 2 | lspsnsubg 20824 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) |
| 17 | 5, 6, 16 | syl2anc 583 |
. . . . . 6
β’ (π β (πβ{π}) β (SubGrpβπ)) |
| 18 | | lspabs3.e |
. . . . . . 7
β’ (π β (πβ{π}) = (πβ{π})) |
| 19 | 18, 17 | eqeltrrd 2828 |
. . . . . 6
β’ (π β (πβ{π}) β (SubGrpβπ)) |
| 20 | 7, 2 | lspsnid 20837 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
| 21 | 5, 6, 20 | syl2anc 583 |
. . . . . 6
β’ (π β π β (πβ{π})) |
| 22 | 7, 2 | lspsnid 20837 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
| 23 | 5, 10, 22 | syl2anc 583 |
. . . . . 6
β’ (π β π β (πβ{π})) |
| 24 | | lspabs2.p |
. . . . . . 7
β’ + =
(+gβπ) |
| 25 | 24, 13 | lsmelvali 19567 |
. . . . . 6
β’ ((((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β§ (π β (πβ{π}) β§ π β (πβ{π}))) β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 26 | 17, 19, 21, 23, 25 | syl22anc 836 |
. . . . 5
β’ (π β (π + π) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 27 | 1, 2, 5, 15, 26 | lspsnel5a 20840 |
. . . 4
β’ (π β (πβ{(π + π)}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 28 | 18 | oveq2d 7420 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 29 | 13 | lsmidm 19580 |
. . . . . 6
β’ ((πβ{π}) β (SubGrpβπ) β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
| 30 | 17, 29 | syl 17 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
| 31 | 28, 30 | eqtr3d 2768 |
. . . 4
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
| 32 | 27, 31 | sseqtrd 4017 |
. . 3
β’ (π β (πβ{(π + π)}) β (πβ{π})) |
| 33 | | lspabs2.o |
. . . 4
β’ 0 =
(0gβπ) |
| 34 | 7, 24 | lmodvacl 20718 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
| 35 | 5, 6, 10, 34 | syl3anc 1368 |
. . . . 5
β’ (π β (π + π) β π) |
| 36 | | lspabs3.xy |
. . . . 5
β’ (π β (π + π) β 0 ) |
| 37 | | eldifsn 4785 |
. . . . 5
β’ ((π + π) β (π β { 0 }) β ((π + π) β π β§ (π + π) β 0 )) |
| 38 | 35, 36, 37 | sylanbrc 582 |
. . . 4
β’ (π β (π + π) β (π β { 0 })) |
| 39 | 7, 33, 2, 3, 38, 6 | lspsncmp 20964 |
. . 3
β’ (π β ((πβ{(π + π)}) β (πβ{π}) β (πβ{(π + π)}) = (πβ{π}))) |
| 40 | 32, 39 | mpbid 231 |
. 2
β’ (π β (πβ{(π + π)}) = (πβ{π})) |
| 41 | 40 | eqcomd 2732 |
1
β’ (π β (πβ{π}) = (πβ{(π + π)})) |
