Theorem ig1pmindeg

Description: The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025)

	Ref	Expression
Hypotheses	ig1pirred.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ig1pirred.g	$$⊢G={idlGen}_{\mathrm{1p}}\left(R\right)$$
	ig1pirred.u	$$⊢U={\mathrm{Base}}_P$$
	ig1pirred.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
	ig1pirred.1	$$⊢\phi \to I\in \mathrm{LIdeal}\left(P\right)$$
	ig1pmindeg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	ig1pmindeg.o	$$⊢\underset{\dot{}}{0}=0_P$$
	ig1pmindeg.2	$$⊢\phi \to F\in I$$
	ig1pmindeg.3	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
Assertion	ig1pmindeg	$$⊢\phi \to D\left(G\left(I\right)\right)\le D\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		ig1pirred.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ig1pirred.g	$$⊢G={idlGen}_{\mathrm{1p}}\left(R\right)$$
3		ig1pirred.u	$$⊢U={\mathrm{Base}}_P$$
4		ig1pirred.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
5		ig1pirred.1	$$⊢\phi \to I\in \mathrm{LIdeal}\left(P\right)$$
6		ig1pmindeg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
7		ig1pmindeg.o	$$⊢\underset{\dot{}}{0}=0_P$$
8		ig1pmindeg.2	$$⊢\phi \to F\in I$$
9		ig1pmindeg.3	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
10	8	adantr	$$⊢\left(\phi \wedge I=\left\{\underset{\dot{}}{0}\right\}\right)\to F\in I$$
11		simpr	$$⊢\left(\phi \wedge I=\left\{\underset{\dot{}}{0}\right\}\right)\to I=\left\{\underset{\dot{}}{0}\right\}$$
12	10 11	eleqtrd	$$⊢\left(\phi \wedge I=\left\{\underset{\dot{}}{0}\right\}\right)\to F\in \left\{\underset{\dot{}}{0}\right\}$$
13		elsni	$$⊢F\in \left\{\underset{\dot{}}{0}\right\}\to F=\underset{\dot{}}{0}$$
14	12 13	syl	$$⊢\left(\phi \wedge I=\left\{\underset{\dot{}}{0}\right\}\right)\to F=\underset{\dot{}}{0}$$
15	9	adantr	$$⊢\left(\phi \wedge I=\left\{\underset{\dot{}}{0}\right\}\right)\to F\ne \underset{\dot{}}{0}$$
16	14 15	pm2.21ddne	$$⊢\left(\phi \wedge I=\left\{\underset{\dot{}}{0}\right\}\right)\to D\left(G\left(I\right)\right)\le D\left(F\right)$$
17	4	adantr	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to R\in \mathrm{DivRing}$$
18	5	adantr	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to I\in \mathrm{LIdeal}\left(P\right)$$
19		simpr	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to I\ne \left\{\underset{\dot{}}{0}\right\}$$
20		eqid	$$⊢\mathrm{LIdeal}\left(P\right)=\mathrm{LIdeal}\left(P\right)$$
21		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(R\right)={Monic}_{\mathrm{1p}}\left(R\right)$$
22	1 2 7 20 6 21	ig1pval3	$$⊢\left(R\in \mathrm{DivRing}\wedge I\in \mathrm{LIdeal}\left(P\right)\wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \left(G\left(I\right)\in I\wedge G\left(I\right)\in {Monic}_{\mathrm{1p}}\left(R\right)\wedge D\left(G\left(I\right)\right)=sup\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)$$
23	17 18 19 22	syl3anc	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \left(G\left(I\right)\in I\wedge G\left(I\right)\in {Monic}_{\mathrm{1p}}\left(R\right)\wedge D\left(G\left(I\right)\right)=sup\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)$$
24	23	simp3d	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to D\left(G\left(I\right)\right)=sup\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)$$
25		nfv	$$⊢Ⅎf\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
26	6 1 3	deg1xrf	$$⊢D:U⟶{ℝ}^{*}$$
27	26	a1i	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to D:U⟶{ℝ}^{*}$$
28	27	ffund	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \mathrm{Fun}D$$
29	17	drngringd	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to R\in \mathrm{Ring}$$
30	29	adantr	$$⊢\left(\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\wedge f\in \left(I\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to R\in \mathrm{Ring}$$
31	3 20	lidlss	$$⊢I\in \mathrm{LIdeal}\left(P\right)\to I\subseteq U$$
32	18 31	syl	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to I\subseteq U$$
33	32	ssdifssd	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to I\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq U$$
34	33	sselda	$$⊢\left(\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\wedge f\in \left(I\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to f\in U$$
35		eldifsni	$$⊢f\in \left(I\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to f\ne \underset{\dot{}}{0}$$
36	35	adantl	$$⊢\left(\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\wedge f\in \left(I\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to f\ne \underset{\dot{}}{0}$$
37	6 1 7 3	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge f\in U\wedge f\ne \underset{\dot{}}{0}\right)\to D\left(f\right)\in {\mathbb{N}}_0$$
38	30 34 36 37	syl3anc	$$⊢\left(\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\wedge f\in \left(I\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to D\left(f\right)\in {\mathbb{N}}_0$$
39		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
40	38 39	eleqtrdi	$$⊢\left(\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\wedge f\in \left(I\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to D\left(f\right)\in {\mathbb{Z}}_{\ge 0}$$
41	25 28 40	funimassd	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq {\mathbb{Z}}_{\ge 0}$$
42	27	ffnd	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to DFnU$$
43	8	adantr	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to F\in I$$
44	32 43	sseldd	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to F\in U$$
45	9	adantr	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to F\ne \underset{\dot{}}{0}$$
46		nelsn	$$⊢F\ne \underset{\dot{}}{0}\to \neg F\in \left\{\underset{\dot{}}{0}\right\}$$
47	45 46	syl	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \neg F\in \left\{\underset{\dot{}}{0}\right\}$$
48	43 47	eldifd	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to F\in \left(I\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
49	42 44 48	fnfvimad	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to D\left(F\right)\in D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
50		infssuzle	$$⊢\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq {\mathbb{Z}}_{\ge 0}\wedge D\left(F\right)\in D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\to sup\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\le D\left(F\right)$$
51	41 49 50	syl2anc	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to sup\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\le D\left(F\right)$$
52	24 51	eqbrtrd	$$⊢\left(\phi \wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to D\left(G\left(I\right)\right)\le D\left(F\right)$$
53	16 52	pm2.61dane	$$⊢\phi \to D\left(G\left(I\right)\right)\le D\left(F\right)$$