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}={\mathrm{Poly}}_{1}\left({R}\right)$
hbtlem.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
hbtlem.s ${⊢}{S}=\mathrm{ldgIdlSeq}\left({R}\right)$
hbtlem2.t ${⊢}{T}=\mathrm{LIdeal}\left({R}\right)$
Assertion hbtlem2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {U}\wedge {X}\in {ℕ}_{0}\right)\to {S}\left({I}\right)\left({X}\right)\in {T}$

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