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=Poly1R
hbtlem.u U=LIdealP
hbtlem.s S=ldgIdlSeqR
hbtlem3.r φRRing
hbtlem3.i φIU
hbtlem3.j φJU
hbtlem3.ij φIJ
hbtlem5.e φx0SJxSIx
Assertion hbtlem5 φI=J

Proof

Step Hyp Ref Expression
1 hbtlem.p P=Poly1R
2 hbtlem.u U=LIdealP
3 hbtlem.s S=ldgIdlSeqR
4 hbtlem3.r φRRing
5 hbtlem3.i φIU
6 hbtlem3.j φJU
7 hbtlem3.ij φIJ
8 hbtlem5.e φx0SJxSIx
9 eqid BaseP=BaseP
10 9 2 lidlss JUJBaseP
11 6 10 syl φJBaseP
12 11 sselda φaJaBaseP
13 eqid deg1R=deg1R
14 13 1 9 deg1cl aBasePdeg1Ra0−∞
15 12 14 syl φaJdeg1Ra0−∞
16 elun deg1Ra0−∞deg1Ra0deg1Ra−∞
17 nnssnn0 0
18 nn0re deg1Ra0deg1Ra
19 arch deg1Rabdeg1Ra<b
20 18 19 syl deg1Ra0bdeg1Ra<b
21 ssrexv 0bdeg1Ra<bb0deg1Ra<b
22 17 20 21 mpsyl deg1Ra0b0deg1Ra<b
23 elsni deg1Ra−∞deg1Ra=−∞
24 0nn0 00
25 mnflt0 −∞<0
26 breq2 b=0−∞<b−∞<0
27 26 rspcev 00−∞<0b0−∞<b
28 24 25 27 mp2an b0−∞<b
29 breq1 deg1Ra=−∞deg1Ra<b−∞<b
30 29 rexbidv deg1Ra=−∞b0deg1Ra<bb0−∞<b
31 28 30 mpbiri deg1Ra=−∞b0deg1Ra<b
32 23 31 syl deg1Ra−∞b0deg1Ra<b
33 22 32 jaoi deg1Ra0deg1Ra−∞b0deg1Ra<b
34 16 33 sylbi deg1Ra0−∞b0deg1Ra<b
35 15 34 syl φaJb0deg1Ra<b
36 breq2 c=0deg1Ra<cdeg1Ra<0
37 36 imbi1d c=0deg1Ra<caIdeg1Ra<0aI
38 37 ralbidv c=0aJdeg1Ra<caIaJdeg1Ra<0aI
39 38 imbi2d c=0φaJdeg1Ra<caIφaJdeg1Ra<0aI
40 breq2 c=bdeg1Ra<cdeg1Ra<b
41 40 imbi1d c=bdeg1Ra<caIdeg1Ra<baI
42 41 ralbidv c=baJdeg1Ra<caIaJdeg1Ra<baI
43 42 imbi2d c=bφaJdeg1Ra<caIφaJdeg1Ra<baI
44 breq2 c=b+1deg1Ra<cdeg1Ra<b+1
45 44 imbi1d c=b+1deg1Ra<caIdeg1Ra<b+1aI
46 45 ralbidv c=b+1aJdeg1Ra<caIaJdeg1Ra<b+1aI
47 fveq2 a=ddeg1Ra=deg1Rd
48 47 breq1d a=ddeg1Ra<b+1deg1Rd<b+1
49 eleq1 a=daIdI
50 48 49 imbi12d a=ddeg1Ra<b+1aIdeg1Rd<b+1dI
51 50 cbvralvw aJdeg1Ra<b+1aIdJdeg1Rd<b+1dI
52 46 51 bitrdi c=b+1aJdeg1Ra<caIdJdeg1Rd<b+1dI
53 52 imbi2d c=b+1φaJdeg1Ra<caIφdJdeg1Rd<b+1dI
54 4 adantr φaJRRing
55 eqid 0P=0P
56 13 1 55 9 deg1lt0 RRingaBasePdeg1Ra<0a=0P
57 54 12 56 syl2anc φaJdeg1Ra<0a=0P
58 1 ply1ring RRingPRing
59 4 58 syl φPRing
60 2 55 lidl0cl PRingIU0PI
61 59 5 60 syl2anc φ0PI
62 eleq1a 0PIa=0PaI
63 61 62 syl φa=0PaI
64 63 adantr φaJa=0PaI
65 57 64 sylbid φaJdeg1Ra<0aI
66 65 ralrimiva φaJdeg1Ra<0aI
67 11 3ad2ant2 b0φaJdeg1Ra<baIJBaseP
68 67 sselda b0φaJdeg1Ra<baIdJdBaseP
69 13 1 9 deg1cl dBasePdeg1Rd0−∞
70 68 69 syl b0φaJdeg1Ra<baIdJdeg1Rd0−∞
71 simpl1 b0φaJdeg1Ra<baIdJb0
72 71 nn0zd b0φaJdeg1Ra<baIdJb
73 degltp1le deg1Rd0−∞bdeg1Rd<b+1deg1Rdb
74 70 72 73 syl2anc b0φaJdeg1Ra<baIdJdeg1Rd<b+1deg1Rdb
75 fveq2 x=bSJx=SJb
76 fveq2 x=bSIx=SIb
77 75 76 sseq12d x=bSJxSIxSJbSIb
78 77 rspcva b0x0SJxSIxSJbSIb
79 8 78 sylan2 b0φSJbSIb
80 4 adantl b0φRRing
81 6 adantl b0φJU
82 simpl b0φb0
83 1 2 3 13 hbtlem1 RRingJUb0SJb=c|eJdeg1Rebc=coe1eb
84 80 81 82 83 syl3anc b0φSJb=c|eJdeg1Rebc=coe1eb
85 5 adantl b0φIU
86 1 2 3 13 hbtlem1 RRingIUb0SIb=c|eIdeg1Rebc=coe1eb
87 80 85 82 86 syl3anc b0φSIb=c|eIdeg1Rebc=coe1eb
88 79 84 87 3sstr3d b0φc|eJdeg1Rebc=coe1ebc|eIdeg1Rebc=coe1eb
89 88 3adant3 b0φaJdeg1Ra<baIc|eJdeg1Rebc=coe1ebc|eIdeg1Rebc=coe1eb
90 89 adantr b0φaJdeg1Ra<baIdJdeg1Rdbc|eJdeg1Rebc=coe1ebc|eIdeg1Rebc=coe1eb
91 simpl dJdeg1RdbdJ
92 simpr dJdeg1Rdbdeg1Rdb
93 eqidd dJdeg1Rdbcoe1db=coe1db
94 fveq2 e=ddeg1Re=deg1Rd
95 94 breq1d e=ddeg1Rebdeg1Rdb
96 fveq2 e=dcoe1e=coe1d
97 96 fveq1d e=dcoe1eb=coe1db
98 97 eqeq2d e=dcoe1db=coe1ebcoe1db=coe1db
99 95 98 anbi12d e=ddeg1Rebcoe1db=coe1ebdeg1Rdbcoe1db=coe1db
100 99 rspcev dJdeg1Rdbcoe1db=coe1dbeJdeg1Rebcoe1db=coe1eb
101 91 92 93 100 syl12anc dJdeg1RdbeJdeg1Rebcoe1db=coe1eb
102 fvex coe1dbV
103 eqeq1 c=coe1dbc=coe1ebcoe1db=coe1eb
104 103 anbi2d c=coe1dbdeg1Rebc=coe1ebdeg1Rebcoe1db=coe1eb
105 104 rexbidv c=coe1dbeJdeg1Rebc=coe1ebeJdeg1Rebcoe1db=coe1eb
106 102 105 elab coe1dbc|eJdeg1Rebc=coe1ebeJdeg1Rebcoe1db=coe1eb
107 101 106 sylibr dJdeg1Rdbcoe1dbc|eJdeg1Rebc=coe1eb
108 107 adantl b0φaJdeg1Ra<baIdJdeg1Rdbcoe1dbc|eJdeg1Rebc=coe1eb
109 90 108 sseldd b0φaJdeg1Ra<baIdJdeg1Rdbcoe1dbc|eIdeg1Rebc=coe1eb
110 104 rexbidv c=coe1dbeIdeg1Rebc=coe1ebeIdeg1Rebcoe1db=coe1eb
111 102 110 elab coe1dbc|eIdeg1Rebc=coe1ebeIdeg1Rebcoe1db=coe1eb
112 simpll2 b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebφ
113 112 59 syl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebPRing
114 ringgrp PRingPGrp
115 113 114 syl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebPGrp
116 112 11 syl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebJBaseP
117 simplrl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdJ
118 116 117 sseldd b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdBaseP
119 9 2 lidlss IUIBaseP
120 5 119 syl φIBaseP
121 112 120 syl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebIBaseP
122 simprl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebeI
123 121 122 sseldd b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebeBaseP
124 eqid +P=+P
125 eqid -P=-P
126 9 124 125 grpnpcan PGrpdBasePeBasePd-Pe+Pe=d
127 115 118 123 126 syl3anc b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebd-Pe+Pe=d
128 5 3ad2ant2 b0φaJdeg1Ra<baIIU
129 128 ad2antrr b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebIU
130 simpll1 b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebb0
131 112 4 syl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebRRing
132 simplrr b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdeg1Rdb
133 simprrl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdeg1Reb
134 eqid coe1d=coe1d
135 eqid coe1e=coe1e
136 simprrr b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebcoe1db=coe1eb
137 13 1 9 125 130 131 118 132 123 133 134 135 136 deg1sublt b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdeg1Rd-Pe<b
138 112 6 syl b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebJU
139 7 3ad2ant2 b0φaJdeg1Ra<baIIJ
140 139 ad2antrr b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebIJ
141 140 122 sseldd b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebeJ
142 2 125 lidlsubcl PRingJUdJeJd-PeJ
143 113 138 117 141 142 syl22anc b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebd-PeJ
144 simpll3 b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebaJdeg1Ra<baI
145 fveq2 a=d-Pedeg1Ra=deg1Rd-Pe
146 145 breq1d a=d-Pedeg1Ra<bdeg1Rd-Pe<b
147 eleq1 a=d-PeaId-PeI
148 146 147 imbi12d a=d-Pedeg1Ra<baIdeg1Rd-Pe<bd-PeI
149 148 rspcva d-PeJaJdeg1Ra<baIdeg1Rd-Pe<bd-PeI
150 143 144 149 syl2anc b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdeg1Rd-Pe<bd-PeI
151 137 150 mpd b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebd-PeI
152 2 124 lidlacl PRingIUd-PeIeId-Pe+PeI
153 113 129 151 122 152 syl22anc b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebd-Pe+PeI
154 127 153 eqeltrrd b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdI
155 154 rexlimdvaa b0φaJdeg1Ra<baIdJdeg1RdbeIdeg1Rebcoe1db=coe1ebdI
156 111 155 syl5bi b0φaJdeg1Ra<baIdJdeg1Rdbcoe1dbc|eIdeg1Rebc=coe1ebdI
157 109 156 mpd b0φaJdeg1Ra<baIdJdeg1RdbdI
158 157 expr b0φaJdeg1Ra<baIdJdeg1RdbdI
159 74 158 sylbid b0φaJdeg1Ra<baIdJdeg1Rd<b+1dI
160 159 ralrimiva b0φaJdeg1Ra<baIdJdeg1Rd<b+1dI
161 160 3exp b0φaJdeg1Ra<baIdJdeg1Rd<b+1dI
162 161 a2d b0φaJdeg1Ra<baIφdJdeg1Rd<b+1dI
163 39 43 53 43 66 162 nn0ind b0φaJdeg1Ra<baI
164 rsp aJdeg1Ra<baIaJdeg1Ra<baI
165 163 164 syl6com φb0aJdeg1Ra<baI
166 165 com23 φaJb0deg1Ra<baI
167 166 imp φaJb0deg1Ra<baI
168 167 rexlimdv φaJb0deg1Ra<baI
169 35 168 mpd φaJaI
170 7 169 eqelssd φI=J