Theorem ig1pnunit

Description: The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025)

	Ref	Expression
Hypotheses	ig1pirred.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ig1pirred.g	⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
	ig1pirred.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	ig1pirred.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	ig1pirred.1	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
	ig1pirred.2	⊢ ( 𝜑 → 𝐼 ≠ 𝑈 )
Assertion	ig1pnunit	⊢ ( 𝜑 → ¬ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ig1pirred.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ig1pirred.g	⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
3		ig1pirred.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		ig1pirred.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5		ig1pirred.1	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
6		ig1pirred.2	⊢ ( 𝜑 → 𝐼 ≠ 𝑈 )
7		eqid	⊢ ( Unit ‘ 𝑃 ) = ( Unit ‘ 𝑃 )
8		simpr	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) )
9		eqid	⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
10	1 2 9	ig1pcl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
11	4 5 10	syl2anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
12	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
13	4	drngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
14	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	13 14	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝑃 ∈ Ring )
17	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
18	3 7 8 12 16 17	lidlunitel	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝐼 = 𝑈 )
19	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝐼 ≠ 𝑈 )
20	19	neneqd	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → ¬ 𝐼 = 𝑈 )
21	18 20	pm2.65da	⊢ ( 𝜑 → ¬ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) )