Step | Hyp | Ref
| Expression |
1 | | mhppwdeg.n |
. 2
β’ (π β π β
β0) |
2 | | oveq1 7368 |
. . . 4
β’ (π₯ = 0 β (π₯ β π) = (0 β π)) |
3 | | oveq2 7369 |
. . . . 5
β’ (π₯ = 0 β (π Β· π₯) = (π Β· 0)) |
4 | 3 | fveq2d 6850 |
. . . 4
β’ (π₯ = 0 β (π»β(π Β· π₯)) = (π»β(π Β· 0))) |
5 | 2, 4 | eleq12d 2828 |
. . 3
β’ (π₯ = 0 β ((π₯ β π) β (π»β(π Β· π₯)) β (0 β π) β (π»β(π Β· 0)))) |
6 | | oveq1 7368 |
. . . 4
β’ (π₯ = π¦ β (π₯ β π) = (π¦ β π)) |
7 | | oveq2 7369 |
. . . . 5
β’ (π₯ = π¦ β (π Β· π₯) = (π Β· π¦)) |
8 | 7 | fveq2d 6850 |
. . . 4
β’ (π₯ = π¦ β (π»β(π Β· π₯)) = (π»β(π Β· π¦))) |
9 | 6, 8 | eleq12d 2828 |
. . 3
β’ (π₯ = π¦ β ((π₯ β π) β (π»β(π Β· π₯)) β (π¦ β π) β (π»β(π Β· π¦)))) |
10 | | oveq1 7368 |
. . . 4
β’ (π₯ = (π¦ + 1) β (π₯ β π) = ((π¦ + 1) β π)) |
11 | | oveq2 7369 |
. . . . 5
β’ (π₯ = (π¦ + 1) β (π Β· π₯) = (π Β· (π¦ + 1))) |
12 | 11 | fveq2d 6850 |
. . . 4
β’ (π₯ = (π¦ + 1) β (π»β(π Β· π₯)) = (π»β(π Β· (π¦ + 1)))) |
13 | 10, 12 | eleq12d 2828 |
. . 3
β’ (π₯ = (π¦ + 1) β ((π₯ β π) β (π»β(π Β· π₯)) β ((π¦ + 1) β π) β (π»β(π Β· (π¦ + 1))))) |
14 | | oveq1 7368 |
. . . 4
β’ (π₯ = π β (π₯ β π) = (π β π)) |
15 | | oveq2 7369 |
. . . . 5
β’ (π₯ = π β (π Β· π₯) = (π Β· π)) |
16 | 15 | fveq2d 6850 |
. . . 4
β’ (π₯ = π β (π»β(π Β· π₯)) = (π»β(π Β· π))) |
17 | 14, 16 | eleq12d 2828 |
. . 3
β’ (π₯ = π β ((π₯ β π) β (π»β(π Β· π₯)) β (π β π) β (π»β(π Β· π)))) |
18 | | mhppwdeg.p |
. . . . . . . . 9
β’ π = (πΌ mPoly π
) |
19 | | mhppwdeg.i |
. . . . . . . . 9
β’ (π β πΌ β π) |
20 | | mhppwdeg.r |
. . . . . . . . 9
β’ (π β π
β Ring) |
21 | 18, 19, 20 | mplsca 21440 |
. . . . . . . 8
β’ (π β π
= (Scalarβπ)) |
22 | 21 | fveq2d 6850 |
. . . . . . 7
β’ (π β (1rβπ
) =
(1rβ(Scalarβπ))) |
23 | 22 | fveq2d 6850 |
. . . . . 6
β’ (π β ((algScβπ)β(1rβπ
)) = ((algScβπ)β(1rβ(Scalarβπ)))) |
24 | | eqid 2733 |
. . . . . . 7
β’
(algScβπ) =
(algScβπ) |
25 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
26 | 18 | mpllmod 21446 |
. . . . . . . 8
β’ ((πΌ β π β§ π
β Ring) β π β LMod) |
27 | 19, 20, 26 | syl2anc 585 |
. . . . . . 7
β’ (π β π β LMod) |
28 | 18 | mplring 21447 |
. . . . . . . 8
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
29 | 19, 20, 28 | syl2anc 585 |
. . . . . . 7
β’ (π β π β Ring) |
30 | 24, 25, 27, 29 | ascl1 21311 |
. . . . . 6
β’ (π β ((algScβπ)β(1rβ(Scalarβπ))) = (1rβπ)) |
31 | 23, 30 | eqtrd 2773 |
. . . . 5
β’ (π β ((algScβπ)β(1rβπ
)) = (1rβπ)) |
32 | | mhppwdeg.h |
. . . . . 6
β’ π» = (πΌ mHomP π
) |
33 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
34 | | eqid 2733 |
. . . . . . . 8
β’
(1rβπ
) = (1rβπ
) |
35 | 33, 34 | ringidcl 19997 |
. . . . . . 7
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
36 | 20, 35 | syl 17 |
. . . . . 6
β’ (π β (1rβπ
) β (Baseβπ
)) |
37 | 32, 18, 24, 33, 19, 20, 36 | mhpsclcl 21560 |
. . . . 5
β’ (π β ((algScβπ)β(1rβπ
)) β (π»β0)) |
38 | 31, 37 | eqeltrrd 2835 |
. . . 4
β’ (π β (1rβπ) β (π»β0)) |
39 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
40 | | mhppwdeg.m |
. . . . . 6
β’ (π β π β
β0) |
41 | | mhppwdeg.x |
. . . . . 6
β’ (π β π β (π»βπ)) |
42 | 32, 18, 39, 19, 20, 40, 41 | mhpmpl 21557 |
. . . . 5
β’ (π β π β (Baseβπ)) |
43 | | mhppwdeg.t |
. . . . . . 7
β’ π = (mulGrpβπ) |
44 | 43, 39 | mgpbas 19910 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
45 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
46 | 43, 45 | ringidval 19923 |
. . . . . 6
β’
(1rβπ) = (0gβπ) |
47 | | mhppwdeg.e |
. . . . . 6
β’ β =
(.gβπ) |
48 | 44, 46, 47 | mulg0 18887 |
. . . . 5
β’ (π β (Baseβπ) β (0 β π) = (1rβπ)) |
49 | 42, 48 | syl 17 |
. . . 4
β’ (π β (0 β π) = (1rβπ)) |
50 | 40 | nn0cnd 12483 |
. . . . . 6
β’ (π β π β β) |
51 | 50 | mul01d 11362 |
. . . . 5
β’ (π β (π Β· 0) = 0) |
52 | 51 | fveq2d 6850 |
. . . 4
β’ (π β (π»β(π Β· 0)) = (π»β0)) |
53 | 38, 49, 52 | 3eltr4d 2849 |
. . 3
β’ (π β (0 β π) β (π»β(π Β· 0))) |
54 | | eqid 2733 |
. . . . 5
β’
(.rβπ) = (.rβπ) |
55 | 19 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β πΌ β π) |
56 | 20 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π
β Ring) |
57 | 40 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π β
β0) |
58 | | simplr 768 |
. . . . . 6
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π¦ β β0) |
59 | 57, 58 | nn0mulcld 12486 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β (π Β· π¦) β
β0) |
60 | | simpr 486 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β (π¦ β π) β (π»β(π Β· π¦))) |
61 | 41 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π β (π»βπ)) |
62 | 32, 18, 54, 55, 56, 59, 57, 60, 61 | mhpmulcl 21562 |
. . . 4
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β ((π¦ β π)(.rβπ)π) β (π»β((π Β· π¦) + π))) |
63 | 43 | ringmgp 19978 |
. . . . . . 7
β’ (π β Ring β π β Mnd) |
64 | 29, 63 | syl 17 |
. . . . . 6
β’ (π β π β Mnd) |
65 | 64 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π β Mnd) |
66 | 42 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π β (Baseβπ)) |
67 | 43, 54 | mgpplusg 19908 |
. . . . . 6
β’
(.rβπ) = (+gβπ) |
68 | 44, 47, 67 | mulgnn0p1 18895 |
. . . . 5
β’ ((π β Mnd β§ π¦ β β0
β§ π β
(Baseβπ)) β
((π¦ + 1) β π) = ((π¦ β π)(.rβπ)π)) |
69 | 65, 58, 66, 68 | syl3anc 1372 |
. . . 4
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β ((π¦ + 1) β π) = ((π¦ β π)(.rβπ)π)) |
70 | 50 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π β β) |
71 | 58 | nn0cnd 12483 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β π¦ β β) |
72 | | 1cnd 11158 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β 1 β β) |
73 | 70, 71, 72 | adddid 11187 |
. . . . . 6
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β (π Β· (π¦ + 1)) = ((π Β· π¦) + (π Β· 1))) |
74 | 70 | mulridd 11180 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β (π Β· 1) = π) |
75 | 74 | oveq2d 7377 |
. . . . . 6
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β ((π Β· π¦) + (π Β· 1)) = ((π Β· π¦) + π)) |
76 | 73, 75 | eqtrd 2773 |
. . . . 5
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β (π Β· (π¦ + 1)) = ((π Β· π¦) + π)) |
77 | 76 | fveq2d 6850 |
. . . 4
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β (π»β(π Β· (π¦ + 1))) = (π»β((π Β· π¦) + π))) |
78 | 62, 69, 77 | 3eltr4d 2849 |
. . 3
β’ (((π β§ π¦ β β0) β§ (π¦ β π) β (π»β(π Β· π¦))) β ((π¦ + 1) β π) β (π»β(π Β· (π¦ + 1)))) |
79 | 5, 9, 13, 17, 53, 78 | nn0indd 12608 |
. 2
β’ ((π β§ π β β0) β (π β π) β (π»β(π Β· π))) |
80 | 1, 79 | mpdan 686 |
1
β’ (π β (π β π) β (π»β(π Β· π))) |