ig1pmindeg

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

	Ref	Expression
Hypotheses	ig1pirred.p	$⊢ P = {Poly}_{1} (R)$
	ig1pirred.g	$⊢ G = {idlGen}_{1p} (R)$
	ig1pirred.u	$⊢ U = {Base}_{P}$
	ig1pirred.r	$⊢ φ \to R \in DivRing$
	ig1pirred.1	$⊢ φ \to I \in LIdeal (P)$
	ig1pmindeg.d	$⊢ D = \deg_{1} (R)$
	ig1pmindeg.o	$⊢ \underset{˙}{0} = 0_{P}$
	ig1pmindeg.2	$⊢ φ \to F \in I$
	ig1pmindeg.3	$⊢ φ \to F \neq \underset{˙}{0}$
Assertion	ig1pmindeg	$⊢ φ \to D (G (I)) \leq D (F)$

Proof

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

Metamath Proof Explorer

Theorem ig1pmindeg

Proof