# 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}={\mathrm{Poly}}_{1}\left({R}\right)$
hbtlem.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
hbtlem.s ${⊢}{S}=\mathrm{ldgIdlSeq}\left({R}\right)$
hbtlem3.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
hbtlem3.i ${⊢}{\phi }\to {I}\in {U}$
hbtlem3.j ${⊢}{\phi }\to {J}\in {U}$
hbtlem3.ij ${⊢}{\phi }\to {I}\subseteq {J}$
hbtlem5.e ${⊢}{\phi }\to \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{S}\left({J}\right)\left({x}\right)\subseteq {S}\left({I}\right)\left({x}\right)$
Assertion hbtlem5 ${⊢}{\phi }\to {I}={J}$

### Proof

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