Step | Hyp | Ref
| Expression |
1 | | hbtlem.p |
. . 3
Poly1 |
2 | | hbtlem.u |
. . 3
LIdeal |
3 | | hbtlem.s |
. . 3
ldgIdlSeq |
4 | | eqid 2622 |
. . 3
deg1 deg1 |
5 | 1, 2, 3, 4 | hbtlem1 37693 |
. 2
deg1
coe1 |
6 | | eqid 2622 |
. . . . . . . . . . . 12
|
7 | 6, 2 | lidlss 19210 |
. . . . . . . . . . 11
|
8 | 7 | 3ad2ant2 1083 |
. . . . . . . . . 10
|
9 | 8 | sselda 3603 |
. . . . . . . . 9
|
10 | | eqid 2622 |
. . . . . . . . . 10
coe1 coe1 |
11 | | eqid 2622 |
. . . . . . . . . 10
|
12 | 10, 6, 1, 11 | coe1f 19581 |
. . . . . . . . 9
coe1 |
13 | 9, 12 | syl 17 |
. . . . . . . 8
coe1 |
14 | | simpl3 1066 |
. . . . . . . 8
|
15 | 13, 14 | ffvelrnd 6360 |
. . . . . . 7
coe1 |
16 | | eleq1a 2696 |
. . . . . . 7
coe1 coe1 |
17 | 15, 16 | syl 17 |
. . . . . 6
coe1 |
18 | 17 | adantld 483 |
. . . . 5
deg1
coe1 |
19 | 18 | rexlimdva 3031 |
. . . 4
deg1 coe1 |
20 | 19 | abssdv 3676 |
. . 3
deg1
coe1 |
21 | 1 | ply1ring 19618 |
. . . . . . . 8
|
22 | 21 | 3ad2ant1 1082 |
. . . . . . 7
|
23 | | simp2 1062 |
. . . . . . 7
|
24 | | eqid 2622 |
. . . . . . . 8
|
25 | 2, 24 | lidl0cl 19212 |
. . . . . . 7
|
26 | 22, 23, 25 | syl2anc 693 |
. . . . . 6
|
27 | 4, 1, 24 | deg1z 23847 |
. . . . . . . 8
deg1 |
28 | 27 | 3ad2ant1 1082 |
. . . . . . 7
deg1 |
29 | | nn0ssre 11296 |
. . . . . . . . . 10
|
30 | | ressxr 10083 |
. . . . . . . . . 10
|
31 | 29, 30 | sstri 3612 |
. . . . . . . . 9
|
32 | | simp3 1063 |
. . . . . . . . 9
|
33 | 31, 32 | sseldi 3601 |
. . . . . . . 8
|
34 | | mnfle 11969 |
. . . . . . . 8
|
35 | 33, 34 | syl 17 |
. . . . . . 7
|
36 | 28, 35 | eqbrtrd 4675 |
. . . . . 6
deg1
|
37 | | eqid 2622 |
. . . . . . . . . 10
|
38 | 1, 24, 37 | coe1z 19633 |
. . . . . . . . 9
coe1 |
39 | 38 | 3ad2ant1 1082 |
. . . . . . . 8
coe1 |
40 | 39 | fveq1d 6193 |
. . . . . . 7
coe1 |
41 | | fvex 6201 |
. . . . . . . . 9
|
42 | 41 | fvconst2 6469 |
. . . . . . . 8
|
43 | 42 | 3ad2ant3 1084 |
. . . . . . 7
|
44 | 40, 43 | eqtr2d 2657 |
. . . . . 6
coe1 |
45 | | fveq2 6191 |
. . . . . . . . 9
deg1 deg1 |
46 | 45 | breq1d 4663 |
. . . . . . . 8
deg1 deg1
|
47 | | fveq2 6191 |
. . . . . . . . . 10
coe1 coe1 |
48 | 47 | fveq1d 6193 |
. . . . . . . . 9
coe1 coe1 |
49 | 48 | eqeq2d 2632 |
. . . . . . . 8
coe1 coe1 |
50 | 46, 49 | anbi12d 747 |
. . . . . . 7
deg1 coe1
deg1
coe1 |
51 | 50 | rspcev 3309 |
. . . . . 6
deg1 coe1 deg1 coe1 |
52 | 26, 36, 44, 51 | syl12anc 1324 |
. . . . 5
deg1 coe1 |
53 | | eqeq1 2626 |
. . . . . . . 8
coe1 coe1 |
54 | 53 | anbi2d 740 |
. . . . . . 7
deg1 coe1
deg1 coe1 |
55 | 54 | rexbidv 3052 |
. . . . . 6
deg1 coe1
deg1 coe1 |
56 | 41, 55 | elab 3350 |
. . . . 5
deg1 coe1
deg1 coe1 |
57 | 52, 56 | sylibr 224 |
. . . 4
deg1
coe1 |
58 | | ne0i 3921 |
. . . 4
deg1 coe1 deg1 coe1 |
59 | 57, 58 | syl 17 |
. . 3
deg1
coe1 |
60 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 |
61 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 |
62 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
algSc algSc |
63 | 1, 62, 11, 6 | ply1sclf 19655 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
algSc |
64 | 63 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
algSc |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1
deg1 algSc |
66 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1
deg1 |
67 | 65, 66 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 algSc |
68 | | simprll 802 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1
deg1 |
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 |
70 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
71 | 2, 6, 70 | lidlmcl 19217 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc algSc |
72 | 60, 61, 67, 69, 71 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 algSc |
73 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 |
74 | 73 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 |
75 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
76 | 2, 75 | lidlacl 19213 |
. . . . . . . . . . . . . . . . . . . . . 22
algSc
algSc |
77 | 60, 61, 72, 74, 76 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . 21
deg1
deg1 algSc |
78 | | simpl1 1064 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 |
79 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1
deg1 |
80 | 79, 69 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 |
81 | 6, 70 | ringcl 18561 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc
algSc |
82 | 60, 67, 80, 81 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 algSc |
83 | 79, 74 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 |
84 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 |
85 | 31, 84 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 |
86 | 4, 1, 6 | deg1xrcl 23842 |
. . . . . . . . . . . . . . . . . . . . . . . 24
algSc
deg1 algSc |
87 | 82, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 deg1 algSc |
88 | 4, 1, 6 | deg1xrcl 23842 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1 |
89 | 80, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 deg1 |
90 | 4, 1, 11, 6, 70, 62 | deg1mul3le 23876 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1 algSc deg1 |
91 | 78, 66, 80, 90 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 deg1 algSc deg1 |
92 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1
deg1
deg1 |
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 deg1 |
94 | 87, 89, 85, 91, 93 | xrletrd 11993 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 deg1 algSc |
95 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1
deg1 |
96 | 95 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 deg1 |
97 | 1, 4, 78, 6, 75, 82, 83, 85, 94, 96 | deg1addle2 23862 |
. . . . . . . . . . . . . . . . . . . . 21
deg1
deg1 deg1 algSc |
98 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | 1, 6, 75, 98 | coe1addfv 19635 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc
coe1algSc coe1algSc coe1 |
100 | 78, 82, 83, 84, 99 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 coe1algSc coe1algSc coe1 |
101 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
102 | 1, 6, 11, 62, 70, 101 | coe1sclmulfv 19653 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1algSc coe1 |
103 | 78, 66, 80, 84, 102 | syl121anc 1331 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 coe1algSc coe1 |
104 | 103 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 coe1algSc coe1 coe1 coe1 |
105 | 100, 104 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . 21
deg1
deg1 coe1 coe1 coe1algSc |
106 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
algSc
deg1 deg1 algSc |
107 | 106 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc deg1 deg1 algSc |
108 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
algSc coe1 coe1algSc |
109 | 108 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
algSc coe1 coe1algSc |
110 | 109 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc coe1 coe1 coe1 coe1 coe1 coe1algSc |
111 | 107, 110 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . 22
algSc deg1
coe1 coe1 coe1
deg1 algSc coe1 coe1 coe1algSc |
112 | 111 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . 21
algSc deg1 algSc coe1 coe1 coe1algSc
deg1 coe1 coe1 coe1 |
113 | 77, 97, 105, 112 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . 20
deg1
deg1 deg1 coe1 coe1 coe1 |
114 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 coe1 |
115 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1
coe1 coe1 coe1 coe1 |
116 | 115 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 coe1
deg1
coe1
deg1 coe1 coe1 coe1 |
117 | 116 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 coe1
deg1
coe1
deg1 coe1 coe1 coe1 |
118 | 114, 117 | elab 3350 |
. . . . . . . . . . . . . . . . . . . 20
coe1 coe1
deg1
coe1
deg1 coe1 coe1 coe1 |
119 | 113, 118 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
deg1
deg1 coe1 coe1 deg1
coe1 |
120 | 119 | exp45 642 |
. . . . . . . . . . . . . . . . . 18
deg1
deg1
coe1 coe1
deg1
coe1 |
121 | 120 | imp 445 |
. . . . . . . . . . . . . . . . 17
deg1
deg1
coe1 coe1
deg1
coe1 |
122 | 121 | exp5c 644 |
. . . . . . . . . . . . . . . 16
deg1
deg1 coe1 coe1
deg1
coe1 |
123 | 122 | imp 445 |
. . . . . . . . . . . . . . 15
deg1 deg1
coe1 coe1
deg1
coe1 |
124 | 123 | imp41 619 |
. . . . . . . . . . . . . 14
deg1
deg1
coe1 coe1
deg1
coe1 |
125 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
coe1 coe1 coe1 coe1 |
126 | 125 | eleq1d 2686 |
. . . . . . . . . . . . . 14
coe1 coe1
deg1
coe1 coe1 coe1
deg1
coe1 |
127 | 124, 126 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
deg1
deg1
coe1 coe1
deg1
coe1 |
128 | 127 | expimpd 629 |
. . . . . . . . . . . 12
deg1
deg1 coe1 coe1
deg1
coe1 |
129 | 128 | rexlimdva 3031 |
. . . . . . . . . . 11
deg1
deg1
coe1 coe1
deg1
coe1 |
130 | 129 | alrimiv 1855 |
. . . . . . . . . 10
deg1
deg1
coe1 coe1
deg1
coe1 |
131 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
coe1 coe1 |
132 | 131 | anbi2d 740 |
. . . . . . . . . . . . 13
deg1 coe1
deg1
coe1 |
133 | 132 | rexbidv 3052 |
. . . . . . . . . . . 12
deg1 coe1
deg1
coe1 |
134 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
deg1 deg1 |
135 | 134 | breq1d 4663 |
. . . . . . . . . . . . . 14
deg1 deg1 |
136 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
coe1 coe1 |
137 | 136 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
coe1 coe1 |
138 | 137 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
coe1 coe1 |
139 | 135, 138 | anbi12d 747 |
. . . . . . . . . . . . 13
deg1 coe1
deg1
coe1 |
140 | 139 | cbvrexv 3172 |
. . . . . . . . . . . 12
deg1
coe1
deg1
coe1 |
141 | 133, 140 | syl6bb 276 |
. . . . . . . . . . 11
deg1 coe1
deg1
coe1 |
142 | 141 | ralab 3367 |
. . . . . . . . . 10
deg1 coe1 coe1
deg1
coe1
deg1
coe1 coe1
deg1
coe1 |
143 | 130, 142 | sylibr 224 |
. . . . . . . . 9
deg1
deg1
coe1 coe1
deg1
coe1 |
144 | | oveq2 6658 |
. . . . . . . . . . . 12
coe1 coe1 |
145 | 144 | oveq1d 6665 |
. . . . . . . . . . 11
coe1 coe1 |
146 | 145 | eleq1d 2686 |
. . . . . . . . . 10
coe1
deg1
coe1 coe1
deg1
coe1 |
147 | 146 | ralbidv 2986 |
. . . . . . . . 9
coe1
deg1
coe1 deg1 coe1
deg1
coe1 coe1
deg1
coe1 |
148 | 143, 147 | syl5ibrcom 237 |
. . . . . . . 8
deg1
coe1
deg1
coe1 deg1 coe1 |
149 | 148 | expimpd 629 |
. . . . . . 7
deg1 coe1
deg1
coe1
deg1
coe1 |
150 | 149 | rexlimdva 3031 |
. . . . . 6
deg1
coe1
deg1
coe1 deg1 coe1 |
151 | 150 | alrimiv 1855 |
. . . . 5
deg1
coe1
deg1
coe1
deg1
coe1 |
152 | | eqeq1 2626 |
. . . . . . . . 9
coe1 coe1 |
153 | 152 | anbi2d 740 |
. . . . . . . 8
deg1 coe1
deg1
coe1 |
154 | 153 | rexbidv 3052 |
. . . . . . 7
deg1 coe1
deg1
coe1 |
155 | | fveq2 6191 |
. . . . . . . . . 10
deg1 deg1 |
156 | 155 | breq1d 4663 |
. . . . . . . . 9
deg1 deg1 |
157 | | fveq2 6191 |
. . . . . . . . . . 11
coe1 coe1 |
158 | 157 | fveq1d 6193 |
. . . . . . . . . 10
coe1 coe1 |
159 | 158 | eqeq2d 2632 |
. . . . . . . . 9
coe1 coe1 |
160 | 156, 159 | anbi12d 747 |
. . . . . . . 8
deg1 coe1
deg1
coe1 |
161 | 160 | cbvrexv 3172 |
. . . . . . 7
deg1
coe1
deg1
coe1 |
162 | 154, 161 | syl6bb 276 |
. . . . . 6
deg1 coe1
deg1
coe1 |
163 | 162 | ralab 3367 |
. . . . 5
deg1 coe1
deg1
coe1 deg1 coe1
deg1
coe1
deg1
coe1
deg1
coe1 |
164 | 151, 163 | sylibr 224 |
. . . 4
deg1
coe1
deg1 coe1 deg1 coe1 |
165 | 164 | ralrimiva 2966 |
. . 3
deg1
coe1
deg1
coe1 deg1 coe1 |
166 | | hbtlem2.t |
. . . 4
LIdeal |
167 | 166, 11, 98, 101 | islidl 19211 |
. . 3
deg1
coe1
deg1
coe1
deg1 coe1
deg1
coe1
deg1
coe1 deg1 coe1 |
168 | 20, 59, 165, 167 | syl3anbrc 1246 |
. 2
deg1
coe1 |
169 | 5, 168 | eqeltrd 2701 |
1
|