Metamath Proof Explorer


Theorem hbtlem2

Description: Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p P = Poly 1 R
hbtlem.u U = LIdeal P
hbtlem.s S = ldgIdlSeq R
hbtlem2.t T = LIdeal R
Assertion hbtlem2 R Ring I U X 0 S I X T

Proof

Step Hyp Ref Expression
1 hbtlem.p P = Poly 1 R
2 hbtlem.u U = LIdeal P
3 hbtlem.s S = ldgIdlSeq R
4 hbtlem2.t T = LIdeal R
5 eqid deg 1 R = deg 1 R
6 1 2 3 5 hbtlem1 R Ring I U X 0 S I X = a | b I deg 1 R b X a = coe 1 b X
7 eqid Base P = Base P
8 7 2 lidlss I U I Base P
9 8 3ad2ant2 R Ring I U X 0 I Base P
10 9 sselda R Ring I U X 0 b I b Base P
11 eqid coe 1 b = coe 1 b
12 eqid Base R = Base R
13 11 7 1 12 coe1f b Base P coe 1 b : 0 Base R
14 10 13 syl R Ring I U X 0 b I coe 1 b : 0 Base R
15 simpl3 R Ring I U X 0 b I X 0
16 14 15 ffvelrnd R Ring I U X 0 b I coe 1 b X Base R
17 eleq1a coe 1 b X Base R a = coe 1 b X a Base R
18 16 17 syl R Ring I U X 0 b I a = coe 1 b X a Base R
19 18 adantld R Ring I U X 0 b I deg 1 R b X a = coe 1 b X a Base R
20 19 rexlimdva R Ring I U X 0 b I deg 1 R b X a = coe 1 b X a Base R
21 20 abssdv R Ring I U X 0 a | b I deg 1 R b X a = coe 1 b X Base R
22 1 ply1ring R Ring P Ring
23 22 3ad2ant1 R Ring I U X 0 P Ring
24 simp2 R Ring I U X 0 I U
25 eqid 0 P = 0 P
26 2 25 lidl0cl P Ring I U 0 P I
27 23 24 26 syl2anc R Ring I U X 0 0 P I
28 5 1 25 deg1z R Ring deg 1 R 0 P = −∞
29 28 3ad2ant1 R Ring I U X 0 deg 1 R 0 P = −∞
30 nn0ssre 0
31 ressxr *
32 30 31 sstri 0 *
33 simp3 R Ring I U X 0 X 0
34 32 33 sseldi R Ring I U X 0 X *
35 mnfle X * −∞ X
36 34 35 syl R Ring I U X 0 −∞ X
37 29 36 eqbrtrd R Ring I U X 0 deg 1 R 0 P X
38 eqid 0 R = 0 R
39 1 25 38 coe1z R Ring coe 1 0 P = 0 × 0 R
40 39 3ad2ant1 R Ring I U X 0 coe 1 0 P = 0 × 0 R
41 40 fveq1d R Ring I U X 0 coe 1 0 P X = 0 × 0 R X
42 fvex 0 R V
43 42 fvconst2 X 0 0 × 0 R X = 0 R
44 43 3ad2ant3 R Ring I U X 0 0 × 0 R X = 0 R
45 41 44 eqtr2d R Ring I U X 0 0 R = coe 1 0 P X
46 fveq2 b = 0 P deg 1 R b = deg 1 R 0 P
47 46 breq1d b = 0 P deg 1 R b X deg 1 R 0 P X
48 fveq2 b = 0 P coe 1 b = coe 1 0 P
49 48 fveq1d b = 0 P coe 1 b X = coe 1 0 P X
50 49 eqeq2d b = 0 P 0 R = coe 1 b X 0 R = coe 1 0 P X
51 47 50 anbi12d b = 0 P deg 1 R b X 0 R = coe 1 b X deg 1 R 0 P X 0 R = coe 1 0 P X
52 51 rspcev 0 P I deg 1 R 0 P X 0 R = coe 1 0 P X b I deg 1 R b X 0 R = coe 1 b X
53 27 37 45 52 syl12anc R Ring I U X 0 b I deg 1 R b X 0 R = coe 1 b X
54 eqeq1 a = 0 R a = coe 1 b X 0 R = coe 1 b X
55 54 anbi2d a = 0 R deg 1 R b X a = coe 1 b X deg 1 R b X 0 R = coe 1 b X
56 55 rexbidv a = 0 R b I deg 1 R b X a = coe 1 b X b I deg 1 R b X 0 R = coe 1 b X
57 42 56 elab 0 R a | b I deg 1 R b X a = coe 1 b X b I deg 1 R b X 0 R = coe 1 b X
58 53 57 sylibr R Ring I U X 0 0 R a | b I deg 1 R b X a = coe 1 b X
59 58 ne0d R Ring I U X 0 a | b I deg 1 R b X a = coe 1 b X
60 23 adantr R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X P Ring
61 simpl2 R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X I U
62 eqid algSc P = algSc P
63 1 62 12 7 ply1sclf R Ring algSc P : Base R Base P
64 63 3ad2ant1 R Ring I U X 0 algSc P : Base R Base P
65 64 adantr R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X algSc P : Base R Base P
66 simprl R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c Base R
67 65 66 ffvelrnd R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X algSc P c Base P
68 simprll c Base R f I deg 1 R f X g I deg 1 R g X f I
69 68 adantl R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X f I
70 eqid P = P
71 2 7 70 lidlmcl P Ring I U algSc P c Base P f I algSc P c P f I
72 60 61 67 69 71 syl22anc R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X algSc P c P f I
73 simprrl c Base R f I deg 1 R f X g I deg 1 R g X g I
74 73 adantl R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X g I
75 eqid + P = + P
76 2 75 lidlacl P Ring I U algSc P c P f I g I algSc P c P f + P g I
77 60 61 72 74 76 syl22anc R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X algSc P c P f + P g I
78 simpl1 R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X R Ring
79 9 adantr R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X I Base P
80 79 69 sseldd R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X f Base P
81 7 70 ringcl P Ring algSc P c Base P f Base P algSc P c P f Base P
82 60 67 80 81 syl3anc R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X algSc P c P f Base P
83 79 74 sseldd R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X g Base P
84 simpl3 R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X X 0
85 32 84 sseldi R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X X *
86 5 1 7 deg1xrcl algSc P c P f Base P deg 1 R algSc P c P f *
87 82 86 syl R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R algSc P c P f *
88 5 1 7 deg1xrcl f Base P deg 1 R f *
89 80 88 syl R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R f *
90 5 1 12 7 70 62 deg1mul3le R Ring c Base R f Base P deg 1 R algSc P c P f deg 1 R f
91 78 66 80 90 syl3anc R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R algSc P c P f deg 1 R f
92 simprlr c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R f X
93 92 adantl R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R f X
94 87 89 85 91 93 xrletrd R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R algSc P c P f X
95 simprrr c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R g X
96 95 adantl R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R g X
97 1 5 78 7 75 82 83 85 94 96 deg1addle2 R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X deg 1 R algSc P c P f + P g X
98 eqid + R = + R
99 1 7 75 98 coe1addfv R Ring algSc P c P f Base P g Base P X 0 coe 1 algSc P c P f + P g X = coe 1 algSc P c P f X + R coe 1 g X
100 78 82 83 84 99 syl31anc R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X coe 1 algSc P c P f + P g X = coe 1 algSc P c P f X + R coe 1 g X
101 eqid R = R
102 1 7 12 62 70 101 coe1sclmulfv R Ring c Base R f Base P X 0 coe 1 algSc P c P f X = c R coe 1 f X
103 78 66 80 84 102 syl121anc R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X coe 1 algSc P c P f X = c R coe 1 f X
104 103 oveq1d R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X coe 1 algSc P c P f X + R coe 1 g X = c R coe 1 f X + R coe 1 g X
105 100 104 eqtr2d R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c R coe 1 f X + R coe 1 g X = coe 1 algSc P c P f + P g X
106 fveq2 b = algSc P c P f + P g deg 1 R b = deg 1 R algSc P c P f + P g
107 106 breq1d b = algSc P c P f + P g deg 1 R b X deg 1 R algSc P c P f + P g X
108 fveq2 b = algSc P c P f + P g coe 1 b = coe 1 algSc P c P f + P g
109 108 fveq1d b = algSc P c P f + P g coe 1 b X = coe 1 algSc P c P f + P g X
110 109 eqeq2d b = algSc P c P f + P g c R coe 1 f X + R coe 1 g X = coe 1 b X c R coe 1 f X + R coe 1 g X = coe 1 algSc P c P f + P g X
111 107 110 anbi12d b = algSc P c P f + P g deg 1 R b X c R coe 1 f X + R coe 1 g X = coe 1 b X deg 1 R algSc P c P f + P g X c R coe 1 f X + R coe 1 g X = coe 1 algSc P c P f + P g X
112 111 rspcev algSc P c P f + P g I deg 1 R algSc P c P f + P g X c R coe 1 f X + R coe 1 g X = coe 1 algSc P c P f + P g X b I deg 1 R b X c R coe 1 f X + R coe 1 g X = coe 1 b X
113 77 97 105 112 syl12anc R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X b I deg 1 R b X c R coe 1 f X + R coe 1 g X = coe 1 b X
114 ovex c R coe 1 f X + R coe 1 g X V
115 eqeq1 a = c R coe 1 f X + R coe 1 g X a = coe 1 b X c R coe 1 f X + R coe 1 g X = coe 1 b X
116 115 anbi2d a = c R coe 1 f X + R coe 1 g X deg 1 R b X a = coe 1 b X deg 1 R b X c R coe 1 f X + R coe 1 g X = coe 1 b X
117 116 rexbidv a = c R coe 1 f X + R coe 1 g X b I deg 1 R b X a = coe 1 b X b I deg 1 R b X c R coe 1 f X + R coe 1 g X = coe 1 b X
118 114 117 elab c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X b I deg 1 R b X c R coe 1 f X + R coe 1 g X = coe 1 b X
119 113 118 sylibr R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X
120 119 exp45 R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X
121 120 imp R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X
122 121 exp5c R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X
123 122 imp R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X
124 123 imp41 R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X
125 oveq2 e = coe 1 g X c R coe 1 f X + R e = c R coe 1 f X + R coe 1 g X
126 125 eleq1d e = coe 1 g X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X c R coe 1 f X + R coe 1 g X a | b I deg 1 R b X a = coe 1 b X
127 124 126 syl5ibrcom R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X e = coe 1 g X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
128 127 expimpd R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X e = coe 1 g X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
129 128 rexlimdva R Ring I U X 0 c Base R f I deg 1 R f X g I deg 1 R g X e = coe 1 g X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
130 129 alrimiv R Ring I U X 0 c Base R f I deg 1 R f X e g I deg 1 R g X e = coe 1 g X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
131 eqeq1 a = e a = coe 1 b X e = coe 1 b X
132 131 anbi2d a = e deg 1 R b X a = coe 1 b X deg 1 R b X e = coe 1 b X
133 132 rexbidv a = e b I deg 1 R b X a = coe 1 b X b I deg 1 R b X e = coe 1 b X
134 fveq2 b = g deg 1 R b = deg 1 R g
135 134 breq1d b = g deg 1 R b X deg 1 R g X
136 fveq2 b = g coe 1 b = coe 1 g
137 136 fveq1d b = g coe 1 b X = coe 1 g X
138 137 eqeq2d b = g e = coe 1 b X e = coe 1 g X
139 135 138 anbi12d b = g deg 1 R b X e = coe 1 b X deg 1 R g X e = coe 1 g X
140 139 cbvrexv b I deg 1 R b X e = coe 1 b X g I deg 1 R g X e = coe 1 g X
141 133 140 syl6bb a = e b I deg 1 R b X a = coe 1 b X g I deg 1 R g X e = coe 1 g X
142 141 ralab e a | b I deg 1 R b X a = coe 1 b X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X e g I deg 1 R g X e = coe 1 g X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
143 130 142 sylibr R Ring I U X 0 c Base R f I deg 1 R f X e a | b I deg 1 R b X a = coe 1 b X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
144 oveq2 d = coe 1 f X c R d = c R coe 1 f X
145 144 oveq1d d = coe 1 f X c R d + R e = c R coe 1 f X + R e
146 145 eleq1d d = coe 1 f X c R d + R e a | b I deg 1 R b X a = coe 1 b X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
147 146 ralbidv d = coe 1 f X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X e a | b I deg 1 R b X a = coe 1 b X c R coe 1 f X + R e a | b I deg 1 R b X a = coe 1 b X
148 143 147 syl5ibrcom R Ring I U X 0 c Base R f I deg 1 R f X d = coe 1 f X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
149 148 expimpd R Ring I U X 0 c Base R f I deg 1 R f X d = coe 1 f X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
150 149 rexlimdva R Ring I U X 0 c Base R f I deg 1 R f X d = coe 1 f X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
151 150 alrimiv R Ring I U X 0 c Base R d f I deg 1 R f X d = coe 1 f X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
152 eqeq1 a = d a = coe 1 b X d = coe 1 b X
153 152 anbi2d a = d deg 1 R b X a = coe 1 b X deg 1 R b X d = coe 1 b X
154 153 rexbidv a = d b I deg 1 R b X a = coe 1 b X b I deg 1 R b X d = coe 1 b X
155 fveq2 b = f deg 1 R b = deg 1 R f
156 155 breq1d b = f deg 1 R b X deg 1 R f X
157 fveq2 b = f coe 1 b = coe 1 f
158 157 fveq1d b = f coe 1 b X = coe 1 f X
159 158 eqeq2d b = f d = coe 1 b X d = coe 1 f X
160 156 159 anbi12d b = f deg 1 R b X d = coe 1 b X deg 1 R f X d = coe 1 f X
161 160 cbvrexv b I deg 1 R b X d = coe 1 b X f I deg 1 R f X d = coe 1 f X
162 154 161 syl6bb a = d b I deg 1 R b X a = coe 1 b X f I deg 1 R f X d = coe 1 f X
163 162 ralab d a | b I deg 1 R b X a = coe 1 b X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X d f I deg 1 R f X d = coe 1 f X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
164 151 163 sylibr R Ring I U X 0 c Base R d a | b I deg 1 R b X a = coe 1 b X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
165 164 ralrimiva R Ring I U X 0 c Base R d a | b I deg 1 R b X a = coe 1 b X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
166 4 12 98 101 islidl a | b I deg 1 R b X a = coe 1 b X T a | b I deg 1 R b X a = coe 1 b X Base R a | b I deg 1 R b X a = coe 1 b X c Base R d a | b I deg 1 R b X a = coe 1 b X e a | b I deg 1 R b X a = coe 1 b X c R d + R e a | b I deg 1 R b X a = coe 1 b X
167 21 59 165 166 syl3anbrc R Ring I U X 0 a | b I deg 1 R b X a = coe 1 b X T
168 6 167 eqeltrd R Ring I U X 0 S I X T