ig1pmindeg

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

	Ref	Expression
Hypotheses	ig1pirred.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	ig1pirred.g	⊢ 𝐺 = ( idlGen_1p ‘ 𝑅 )
	ig1pirred.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	ig1pirred.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	ig1pirred.1	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
	ig1pmindeg.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
	ig1pmindeg.o	⊢ 0 = ( 0_g ‘ 𝑃 )
	ig1pmindeg.2	⊢ ( 𝜑 → 𝐹 ∈ 𝐼 )
	ig1pmindeg.3	⊢ ( 𝜑 → 𝐹 ≠ 0 )
Assertion	ig1pmindeg	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐺 ‘ 𝐼 ) ) ≤ ( 𝐷 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ig1pirred.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		ig1pirred.g	⊢ 𝐺 = ( idlGen_1p ‘ 𝑅 )
3		ig1pirred.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		ig1pirred.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5		ig1pirred.1	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
6		ig1pmindeg.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
7		ig1pmindeg.o	⊢ 0 = ( 0_g ‘ 𝑃 )
8		ig1pmindeg.2	⊢ ( 𝜑 → 𝐹 ∈ 𝐼 )
9		ig1pmindeg.3	⊢ ( 𝜑 → 𝐹 ≠ 0 )
10	8	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = { 0 } ) → 𝐹 ∈ 𝐼 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐼 = { 0 } ) → 𝐼 = { 0 } )
12	10 11	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐼 = { 0 } ) → 𝐹 ∈ { 0 } )
13		elsni	⊢ ( 𝐹 ∈ { 0 } → 𝐹 = 0 )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝐼 = { 0 } ) → 𝐹 = 0 )
15	9	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = { 0 } ) → 𝐹 ≠ 0 )
16	14 15	pm2.21ddne	⊢ ( ( 𝜑 ∧ 𝐼 = { 0 } ) → ( 𝐷 ‘ ( 𝐺 ‘ 𝐼 ) ) ≤ ( 𝐷 ‘ 𝐹 ) )
17	4	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝑅 ∈ DivRing )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
19		simpr	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐼 ≠ { 0 } )
20		eqid	⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
21		eqid	⊢ ( Monic_1p ‘ 𝑅 ) = ( Monic_1p ‘ 𝑅 )
22	1 2 7 20 6 21	ig1pval3	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑃 ) ∧ 𝐼 ≠ { 0 } ) → ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Monic_1p ‘ 𝑅 ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
23	17 18 19 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Monic_1p ‘ 𝑅 ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
24	23	simp3d	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 ‘ ( 𝐺 ‘ 𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
25		nfv	⊢ Ⅎ 𝑓 ( 𝜑 ∧ 𝐼 ≠ { 0 } )
26	6 1 3	deg1xrf	⊢ 𝐷 : 𝑈 ⟶ ℝ^*
27	26	a1i	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐷 : 𝑈 ⟶ ℝ^* )
28	27	ffund	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → Fun 𝐷 )
29	17	drngringd	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝑅 ∈ Ring )
30	29	adantr	⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) ∧ 𝑓 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
31	3 20	lidlss	⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑃 ) → 𝐼 ⊆ 𝑈 )
32	18 31	syl	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐼 ⊆ 𝑈 )
33	32	ssdifssd	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → ( 𝐼 ∖ { 0 } ) ⊆ 𝑈 )
34	33	sselda	⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) ∧ 𝑓 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑓 ∈ 𝑈 )
35		eldifsni	⊢ ( 𝑓 ∈ ( 𝐼 ∖ { 0 } ) → 𝑓 ≠ 0 )
36	35	adantl	⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) ∧ 𝑓 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑓 ≠ 0 )
37	6 1 7 3	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑓 ≠ 0 ) → ( 𝐷 ‘ 𝑓 ) ∈ ℕ₀ )
38	30 34 36 37	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) ∧ 𝑓 ∈ ( 𝐼 ∖ { 0 } ) ) → ( 𝐷 ‘ 𝑓 ) ∈ ℕ₀ )
39		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
40	38 39	eleqtrdi	⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) ∧ 𝑓 ∈ ( 𝐼 ∖ { 0 } ) ) → ( 𝐷 ‘ 𝑓 ) ∈ ( ℤ_≥ ‘ 0 ) )
41	25 28 40	funimassd	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( ℤ_≥ ‘ 0 ) )
42	27	ffnd	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐷 Fn 𝑈 )
43	8	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐹 ∈ 𝐼 )
44	32 43	sseldd	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐹 ∈ 𝑈 )
45	9	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐹 ≠ 0 )
46		nelsn	⊢ ( 𝐹 ≠ 0 → ¬ 𝐹 ∈ { 0 } )
47	45 46	syl	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → ¬ 𝐹 ∈ { 0 } )
48	43 47	eldifd	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → 𝐹 ∈ ( 𝐼 ∖ { 0 } ) )
49	42 44 48	fnfvimad	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 ‘ 𝐹 ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) )
50		infssuzle	⊢ ( ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( ℤ_≥ ‘ 0 ) ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ≤ ( 𝐷 ‘ 𝐹 ) )
51	41 49 50	syl2anc	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ≤ ( 𝐷 ‘ 𝐹 ) )
52	24 51	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 ‘ ( 𝐺 ‘ 𝐼 ) ) ≤ ( 𝐷 ‘ 𝐹 ) )
53	16 52	pm2.61dane	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐺 ‘ 𝐼 ) ) ≤ ( 𝐷 ‘ 𝐹 ) )

Metamath Proof Explorer

Theorem ig1pmindeg

Proof