Theorem ig1pnunit

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

	Ref	Expression
Hypotheses	ig1pirred.p	|- P = ( Poly1 ` R )
	ig1pirred.g	|- G = ( idlGen1p ` R )
	ig1pirred.u	|- U = ( Base ` P )
	ig1pirred.r	|- ( ph -> R e. DivRing )
	ig1pirred.1	|- ( ph -> I e. ( LIdeal ` P ) )
	ig1pirred.2	|- ( ph -> I =/= U )
Assertion	ig1pnunit	|- ( ph -> -. ( G ` I ) e. ( Unit ` P ) )

Proof

Step	Hyp	Ref	Expression
1		ig1pirred.p	|- P = ( Poly1 ` R )
2		ig1pirred.g	|- G = ( idlGen1p ` R )
3		ig1pirred.u	|- U = ( Base ` P )
4		ig1pirred.r	|- ( ph -> R e. DivRing )
5		ig1pirred.1	|- ( ph -> I e. ( LIdeal ` P ) )
6		ig1pirred.2	|- ( ph -> I =/= U )
7		eqid	|- ( Unit ` P ) = ( Unit ` P )
8		simpr	|- ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> ( G ` I ) e. ( Unit ` P ) )
9		eqid	|- ( LIdeal ` P ) = ( LIdeal ` P )
10	1 2 9	ig1pcl	|- ( ( R e. DivRing /\ I e. ( LIdeal ` P ) ) -> ( G ` I ) e. I )
11	4 5 10	syl2anc	|- ( ph -> ( G ` I ) e. I )
12	11	adantr	|- ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> ( G ` I ) e. I )
13	4	drngringd	|- ( ph -> R e. Ring )
14	1	ply1ring	|- ( R e. Ring -> P e. Ring )
15	13 14	syl	|- ( ph -> P e. Ring )
16	15	adantr	|- ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> P e. Ring )
17	5	adantr	|- ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> I e. ( LIdeal ` P ) )
18	3 7 8 12 16 17	lidlunitel	|- ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> I = U )
19	6	adantr	|- ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> I =/= U )
20	19	neneqd	|- ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> -. I = U )
21	18 20	pm2.65da	|- ( ph -> -. ( G ` I ) e. ( Unit ` P ) )