Metamath Proof Explorer


Theorem hbtlem5

Description: The leading ideal function is strictly monotone. (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
hbtlem3.r φ R Ring
hbtlem3.i φ I U
hbtlem3.j φ J U
hbtlem3.ij φ I J
hbtlem5.e φ x 0 S J x S I x
Assertion hbtlem5 φ I = J

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 hbtlem3.r φ R Ring
5 hbtlem3.i φ I U
6 hbtlem3.j φ J U
7 hbtlem3.ij φ I J
8 hbtlem5.e φ x 0 S J x S I x
9 eqid Base P = Base P
10 9 2 lidlss J U J Base P
11 6 10 syl φ J Base P
12 11 sselda φ a J a Base P
13 eqid deg 1 R = deg 1 R
14 13 1 9 deg1cl a Base P deg 1 R a 0 −∞
15 12 14 syl φ a J deg 1 R a 0 −∞
16 elun deg 1 R a 0 −∞ deg 1 R a 0 deg 1 R a −∞
17 nnssnn0 0
18 nn0re deg 1 R a 0 deg 1 R a
19 arch deg 1 R a b deg 1 R a < b
20 18 19 syl deg 1 R a 0 b deg 1 R a < b
21 ssrexv 0 b deg 1 R a < b b 0 deg 1 R a < b
22 17 20 21 mpsyl deg 1 R a 0 b 0 deg 1 R a < b
23 elsni deg 1 R a −∞ deg 1 R a = −∞
24 0nn0 0 0
25 mnflt0 −∞ < 0
26 breq2 b = 0 −∞ < b −∞ < 0
27 26 rspcev 0 0 −∞ < 0 b 0 −∞ < b
28 24 25 27 mp2an b 0 −∞ < b
29 breq1 deg 1 R a = −∞ deg 1 R a < b −∞ < b
30 29 rexbidv deg 1 R a = −∞ b 0 deg 1 R a < b b 0 −∞ < b
31 28 30 mpbiri deg 1 R a = −∞ b 0 deg 1 R a < b
32 23 31 syl deg 1 R a −∞ b 0 deg 1 R a < b
33 22 32 jaoi deg 1 R a 0 deg 1 R a −∞ b 0 deg 1 R a < b
34 16 33 sylbi deg 1 R a 0 −∞ b 0 deg 1 R a < b
35 15 34 syl φ a J b 0 deg 1 R a < b
36 breq2 c = 0 deg 1 R a < c deg 1 R a < 0
37 36 imbi1d c = 0 deg 1 R a < c a I deg 1 R a < 0 a I
38 37 ralbidv c = 0 a J deg 1 R a < c a I a J deg 1 R a < 0 a I
39 38 imbi2d c = 0 φ a J deg 1 R a < c a I φ a J deg 1 R a < 0 a I
40 breq2 c = b deg 1 R a < c deg 1 R a < b
41 40 imbi1d c = b deg 1 R a < c a I deg 1 R a < b a I
42 41 ralbidv c = b a J deg 1 R a < c a I a J deg 1 R a < b a I
43 42 imbi2d c = b φ a J deg 1 R a < c a I φ a J deg 1 R a < b a I
44 breq2 c = b + 1 deg 1 R a < c deg 1 R a < b + 1
45 44 imbi1d c = b + 1 deg 1 R a < c a I deg 1 R a < b + 1 a I
46 45 ralbidv c = b + 1 a J deg 1 R a < c a I a J deg 1 R a < b + 1 a I
47 fveq2 a = d deg 1 R a = deg 1 R d
48 47 breq1d a = d deg 1 R a < b + 1 deg 1 R d < b + 1
49 eleq1 a = d a I d I
50 48 49 imbi12d a = d deg 1 R a < b + 1 a I deg 1 R d < b + 1 d I
51 50 cbvralvw a J deg 1 R a < b + 1 a I d J deg 1 R d < b + 1 d I
52 46 51 bitrdi c = b + 1 a J deg 1 R a < c a I d J deg 1 R d < b + 1 d I
53 52 imbi2d c = b + 1 φ a J deg 1 R a < c a I φ d J deg 1 R d < b + 1 d I
54 4 adantr φ a J R Ring
55 eqid 0 P = 0 P
56 13 1 55 9 deg1lt0 R Ring a Base P deg 1 R a < 0 a = 0 P
57 54 12 56 syl2anc φ a J deg 1 R a < 0 a = 0 P
58 1 ply1ring R Ring P Ring
59 4 58 syl φ P Ring
60 2 55 lidl0cl P Ring I U 0 P I
61 59 5 60 syl2anc φ 0 P I
62 eleq1a 0 P I a = 0 P a I
63 61 62 syl φ a = 0 P a I
64 63 adantr φ a J a = 0 P a I
65 57 64 sylbid φ a J deg 1 R a < 0 a I
66 65 ralrimiva φ a J deg 1 R a < 0 a I
67 11 3ad2ant2 b 0 φ a J deg 1 R a < b a I J Base P
68 67 sselda b 0 φ a J deg 1 R a < b a I d J d Base P
69 13 1 9 deg1cl d Base P deg 1 R d 0 −∞
70 68 69 syl b 0 φ a J deg 1 R a < b a I d J deg 1 R d 0 −∞
71 simpl1 b 0 φ a J deg 1 R a < b a I d J b 0
72 71 nn0zd b 0 φ a J deg 1 R a < b a I d J b
73 degltp1le deg 1 R d 0 −∞ b deg 1 R d < b + 1 deg 1 R d b
74 70 72 73 syl2anc b 0 φ a J deg 1 R a < b a I d J deg 1 R d < b + 1 deg 1 R d b
75 fveq2 x = b S J x = S J b
76 fveq2 x = b S I x = S I b
77 75 76 sseq12d x = b S J x S I x S J b S I b
78 77 rspcva b 0 x 0 S J x S I x S J b S I b
79 8 78 sylan2 b 0 φ S J b S I b
80 4 adantl b 0 φ R Ring
81 6 adantl b 0 φ J U
82 simpl b 0 φ b 0
83 1 2 3 13 hbtlem1 R Ring J U b 0 S J b = c | e J deg 1 R e b c = coe 1 e b
84 80 81 82 83 syl3anc b 0 φ S J b = c | e J deg 1 R e b c = coe 1 e b
85 5 adantl b 0 φ I U
86 1 2 3 13 hbtlem1 R Ring I U b 0 S I b = c | e I deg 1 R e b c = coe 1 e b
87 80 85 82 86 syl3anc b 0 φ S I b = c | e I deg 1 R e b c = coe 1 e b
88 79 84 87 3sstr3d b 0 φ c | e J deg 1 R e b c = coe 1 e b c | e I deg 1 R e b c = coe 1 e b
89 88 3adant3 b 0 φ a J deg 1 R a < b a I c | e J deg 1 R e b c = coe 1 e b c | e I deg 1 R e b c = coe 1 e b
90 89 adantr b 0 φ a J deg 1 R a < b a I d J deg 1 R d b c | e J deg 1 R e b c = coe 1 e b c | e I deg 1 R e b c = coe 1 e b
91 simpl d J deg 1 R d b d J
92 simpr d J deg 1 R d b deg 1 R d b
93 eqidd d J deg 1 R d b coe 1 d b = coe 1 d b
94 fveq2 e = d deg 1 R e = deg 1 R d
95 94 breq1d e = d deg 1 R e b deg 1 R d b
96 fveq2 e = d coe 1 e = coe 1 d
97 96 fveq1d e = d coe 1 e b = coe 1 d b
98 97 eqeq2d e = d coe 1 d b = coe 1 e b coe 1 d b = coe 1 d b
99 95 98 anbi12d e = d deg 1 R e b coe 1 d b = coe 1 e b deg 1 R d b coe 1 d b = coe 1 d b
100 99 rspcev d J deg 1 R d b coe 1 d b = coe 1 d b e J deg 1 R e b coe 1 d b = coe 1 e b
101 91 92 93 100 syl12anc d J deg 1 R d b e J deg 1 R e b coe 1 d b = coe 1 e b
102 fvex coe 1 d b V
103 eqeq1 c = coe 1 d b c = coe 1 e b coe 1 d b = coe 1 e b
104 103 anbi2d c = coe 1 d b deg 1 R e b c = coe 1 e b deg 1 R e b coe 1 d b = coe 1 e b
105 104 rexbidv c = coe 1 d b e J deg 1 R e b c = coe 1 e b e J deg 1 R e b coe 1 d b = coe 1 e b
106 102 105 elab coe 1 d b c | e J deg 1 R e b c = coe 1 e b e J deg 1 R e b coe 1 d b = coe 1 e b
107 101 106 sylibr d J deg 1 R d b coe 1 d b c | e J deg 1 R e b c = coe 1 e b
108 107 adantl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b coe 1 d b c | e J deg 1 R e b c = coe 1 e b
109 90 108 sseldd b 0 φ a J deg 1 R a < b a I d J deg 1 R d b coe 1 d b c | e I deg 1 R e b c = coe 1 e b
110 104 rexbidv c = coe 1 d b e I deg 1 R e b c = coe 1 e b e I deg 1 R e b coe 1 d b = coe 1 e b
111 102 110 elab coe 1 d b c | e I deg 1 R e b c = coe 1 e b e I deg 1 R e b coe 1 d b = coe 1 e b
112 simpll2 b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b φ
113 112 59 syl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b P Ring
114 ringgrp P Ring P Grp
115 113 114 syl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b P Grp
116 112 11 syl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b J Base P
117 simplrl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d J
118 116 117 sseldd b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d Base P
119 9 2 lidlss I U I Base P
120 5 119 syl φ I Base P
121 112 120 syl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b I Base P
122 simprl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b e I
123 121 122 sseldd b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b e Base P
124 eqid + P = + P
125 eqid - P = - P
126 9 124 125 grpnpcan P Grp d Base P e Base P d - P e + P e = d
127 115 118 123 126 syl3anc b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d - P e + P e = d
128 5 3ad2ant2 b 0 φ a J deg 1 R a < b a I I U
129 128 ad2antrr b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b I U
130 simpll1 b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b b 0
131 112 4 syl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b R Ring
132 simplrr b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b deg 1 R d b
133 simprrl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b deg 1 R e b
134 eqid coe 1 d = coe 1 d
135 eqid coe 1 e = coe 1 e
136 simprrr b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b coe 1 d b = coe 1 e b
137 13 1 9 125 130 131 118 132 123 133 134 135 136 deg1sublt b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b deg 1 R d - P e < b
138 112 6 syl b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b J U
139 7 3ad2ant2 b 0 φ a J deg 1 R a < b a I I J
140 139 ad2antrr b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b I J
141 140 122 sseldd b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b e J
142 2 125 lidlsubcl P Ring J U d J e J d - P e J
143 113 138 117 141 142 syl22anc b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d - P e J
144 simpll3 b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b a J deg 1 R a < b a I
145 fveq2 a = d - P e deg 1 R a = deg 1 R d - P e
146 145 breq1d a = d - P e deg 1 R a < b deg 1 R d - P e < b
147 eleq1 a = d - P e a I d - P e I
148 146 147 imbi12d a = d - P e deg 1 R a < b a I deg 1 R d - P e < b d - P e I
149 148 rspcva d - P e J a J deg 1 R a < b a I deg 1 R d - P e < b d - P e I
150 143 144 149 syl2anc b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b deg 1 R d - P e < b d - P e I
151 137 150 mpd b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d - P e I
152 2 124 lidlacl P Ring I U d - P e I e I d - P e + P e I
153 113 129 151 122 152 syl22anc b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d - P e + P e I
154 127 153 eqeltrrd b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d I
155 154 rexlimdvaa b 0 φ a J deg 1 R a < b a I d J deg 1 R d b e I deg 1 R e b coe 1 d b = coe 1 e b d I
156 111 155 syl5bi b 0 φ a J deg 1 R a < b a I d J deg 1 R d b coe 1 d b c | e I deg 1 R e b c = coe 1 e b d I
157 109 156 mpd b 0 φ a J deg 1 R a < b a I d J deg 1 R d b d I
158 157 expr b 0 φ a J deg 1 R a < b a I d J deg 1 R d b d I
159 74 158 sylbid b 0 φ a J deg 1 R a < b a I d J deg 1 R d < b + 1 d I
160 159 ralrimiva b 0 φ a J deg 1 R a < b a I d J deg 1 R d < b + 1 d I
161 160 3exp b 0 φ a J deg 1 R a < b a I d J deg 1 R d < b + 1 d I
162 161 a2d b 0 φ a J deg 1 R a < b a I φ d J deg 1 R d < b + 1 d I
163 39 43 53 43 66 162 nn0ind b 0 φ a J deg 1 R a < b a I
164 rsp a J deg 1 R a < b a I a J deg 1 R a < b a I
165 163 164 syl6com φ b 0 a J deg 1 R a < b a I
166 165 com23 φ a J b 0 deg 1 R a < b a I
167 166 imp φ a J b 0 deg 1 R a < b a I
168 167 rexlimdv φ a J b 0 deg 1 R a < b a I
169 35 168 mpd φ a J a I
170 7 169 eqelssd φ I = J