Step | Hyp | Ref
| Expression |
1 | | hbtlem4.r |
. . . . . . . . . 10
β’ (π β π
β Ring) |
2 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π
β Ring) |
3 | | hbtlem.p |
. . . . . . . . . 10
β’ π = (Poly1βπ
) |
4 | 3 | ply1ring 21635 |
. . . . . . . . 9
β’ (π
β Ring β π β Ring) |
5 | 2, 4 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β Ring) |
6 | | hbtlem4.i |
. . . . . . . . 9
β’ (π β πΌ β π) |
7 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β πΌ β π) |
8 | | eqid 2737 |
. . . . . . . . . 10
β’
(mulGrpβπ) =
(mulGrpβπ) |
9 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
10 | 8, 9 | mgpbas 19909 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
11 | | eqid 2737 |
. . . . . . . . 9
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
12 | 8 | ringmgp 19977 |
. . . . . . . . . 10
β’ (π β Ring β
(mulGrpβπ) β
Mnd) |
13 | 5, 12 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (mulGrpβπ) β Mnd) |
14 | | hbtlem4.x |
. . . . . . . . . . 11
β’ (π β π β
β0) |
15 | 14 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β
β0) |
16 | | hbtlem4.y |
. . . . . . . . . . 11
β’ (π β π β
β0) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β
β0) |
18 | | hbtlem4.xy |
. . . . . . . . . . 11
β’ (π β π β€ π) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β€ π) |
20 | | nn0sub2 12571 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β (π β π) β
β0) |
21 | 15, 17, 19, 20 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (π β π) β
β0) |
22 | | eqid 2737 |
. . . . . . . . . . 11
β’
(var1βπ
) = (var1βπ
) |
23 | 22, 3, 9 | vr1cl 21604 |
. . . . . . . . . 10
β’ (π
β Ring β
(var1βπ
)
β (Baseβπ)) |
24 | 2, 23 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (var1βπ
) β (Baseβπ)) |
25 | 10, 11, 13, 21, 24 | mulgnn0cld 18904 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β ((π β π)(.gβ(mulGrpβπ))(var1βπ
)) β (Baseβπ)) |
26 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β πΌ) |
27 | | hbtlem.u |
. . . . . . . . 9
β’ π = (LIdealβπ) |
28 | | eqid 2737 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
29 | 27, 9, 28 | lidlmcl 20703 |
. . . . . . . 8
β’ (((π β Ring β§ πΌ β π) β§ (((π β π)(.gβ(mulGrpβπ))(var1βπ
)) β (Baseβπ) β§ π β πΌ)) β (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β πΌ) |
30 | 5, 7, 25, 26, 29 | syl22anc 838 |
. . . . . . 7
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β πΌ) |
31 | | eqid 2737 |
. . . . . . . . 9
β’ (
deg1 βπ
) =
( deg1 βπ
) |
32 | 9, 27 | lidlss 20696 |
. . . . . . . . . . 11
β’ (πΌ β π β πΌ β (Baseβπ)) |
33 | 7, 32 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β πΌ β (Baseβπ)) |
34 | 33, 26 | sseldd 3950 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β (Baseβπ)) |
35 | 31, 3, 22, 8, 11 | deg1pwle 25500 |
. . . . . . . . . 10
β’ ((π
β Ring β§ (π β π) β β0) β ((
deg1 βπ
)β((π β π)(.gβ(mulGrpβπ))(var1βπ
))) β€ (π β π)) |
36 | 2, 21, 35 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (( deg1 βπ
)β((π β π)(.gβ(mulGrpβπ))(var1βπ
))) β€ (π β π)) |
37 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (( deg1 βπ
)βπ) β€ π) |
38 | 3, 31, 2, 9, 28, 25, 34, 21, 15, 36, 37 | deg1mulle2 25490 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (( deg1 βπ
)β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π)) β€ ((π β π) + π)) |
39 | 17 | nn0cnd 12482 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β β) |
40 | 15 | nn0cnd 12482 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β π β β) |
41 | 39, 40 | npcand 11523 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β ((π β π) + π) = π) |
42 | 38, 41 | breqtrd 5136 |
. . . . . . 7
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (( deg1 βπ
)β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π)) β€ π) |
43 | | eqid 2737 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
44 | 43, 3, 22, 8, 11, 9, 28, 2, 34, 21, 15 | coe1pwmulfv 21667 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))β((π β π) + π)) = ((coe1βπ)βπ)) |
45 | 41 | fveq2d 6851 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))β((π β π) + π)) = ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))βπ)) |
46 | 44, 45 | eqtr3d 2779 |
. . . . . . 7
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β ((coe1βπ)βπ) = ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))βπ)) |
47 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β (( deg1 βπ
)βπ) = (( deg1 βπ
)β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))) |
48 | 47 | breq1d 5120 |
. . . . . . . . 9
β’ (π = (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β ((( deg1 βπ
)βπ) β€ π β (( deg1 βπ
)β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π)) β€ π)) |
49 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β (coe1βπ) =
(coe1β(((π
β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))) |
50 | 49 | fveq1d 6849 |
. . . . . . . . . 10
β’ (π = (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β ((coe1βπ)βπ) = ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))βπ)) |
51 | 50 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β (((coe1βπ)βπ) = ((coe1βπ)βπ) β ((coe1βπ)βπ) = ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))βπ))) |
52 | 48, 51 | anbi12d 632 |
. . . . . . . 8
β’ (π = (((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β (((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)) β ((( deg1 βπ
)β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π)) β€ π β§ ((coe1βπ)βπ) = ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))βπ)))) |
53 | 52 | rspcev 3584 |
. . . . . . 7
β’
(((((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π) β πΌ β§ ((( deg1 βπ
)β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π)) β€ π β§ ((coe1βπ)βπ) = ((coe1β(((π β π)(.gβ(mulGrpβπ))(var1βπ
))(.rβπ)π))βπ))) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
54 | 30, 42, 46, 53 | syl12anc 836 |
. . . . . 6
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
55 | | eqeq1 2741 |
. . . . . . . 8
β’ (π = ((coe1βπ)βπ) β (π = ((coe1βπ)βπ) β ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
56 | 55 | anbi2d 630 |
. . . . . . 7
β’ (π = ((coe1βπ)βπ) β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) |
57 | 56 | rexbidv 3176 |
. . . . . 6
β’ (π = ((coe1βπ)βπ) β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) |
58 | 54, 57 | syl5ibrcom 247 |
. . . . 5
β’ (((π β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (π = ((coe1βπ)βπ) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
59 | 58 | expimpd 455 |
. . . 4
β’ ((π β§ π β πΌ) β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
60 | 59 | rexlimdva 3153 |
. . 3
β’ (π β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
61 | 60 | ss2abdv 4025 |
. 2
β’ (π β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
62 | | hbtlem.s |
. . . 4
β’ π = (ldgIdlSeqβπ
) |
63 | 3, 27, 62, 31 | hbtlem1 41479 |
. . 3
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
64 | 1, 6, 14, 63 | syl3anc 1372 |
. 2
β’ (π β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
65 | 3, 27, 62, 31 | hbtlem1 41479 |
. . 3
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
66 | 1, 6, 16, 65 | syl3anc 1372 |
. 2
β’ (π β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
67 | 61, 64, 66 | 3sstr4d 3996 |
1
β’ (π β ((πβπΌ)βπ) β ((πβπΌ)βπ)) |