Theorem ply1annnr

Description: The set Q of polynomials annihilating an element A is not the whole polynomial ring. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	ply1annidl.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
	ply1annidl.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
	ply1annidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ply1annidl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	ply1annidl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	ply1annidl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	ply1annidl.0	⊢ 0 = ( 0g ‘ 𝑅 )
	ply1annidl.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
	ply1annnr.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	ply1annnr.1	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion	ply1annnr	⊢ ( 𝜑 → 𝑄 ≠ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ply1annidl.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2		ply1annidl.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3		ply1annidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		ply1annidl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		ply1annidl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
6		ply1annidl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		ply1annidl.0	⊢ 0 = ( 0g ‘ 𝑅 )
8		ply1annidl.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9		ply1annnr.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
10		ply1annnr.1	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
11	8	a1i	⊢ ( 𝜑 → 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
12	4	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
13		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
14	13	subrg1cl	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
15	5 14	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
16	3	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
17	5 16	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
18		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
19	18 3 13	ress1r	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
20	12 15 17 19	syl3anc	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
21	20	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
22		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
23		eqid	⊢ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) )
24		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
25	18	subrgring	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
26	5 25	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
27	2 22 23 24 26	ply1ascl1	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 1r ‘ 𝑃 ) )
28	21 27	eqtrd	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
29	2	ply1ring	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ Ring )
30	9 24	ringidcl	⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
31	26 29 30	3syl	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
32	28 31	eqeltrd	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝑈 )
33	1 2 18 3 22 4 5 15 6	evls1scafv	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = ( 1r ‘ 𝑅 ) )
34	13 7	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
35	10 34	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
36	33 35	eqnetrd	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) ≠ 0 )
37	36	neneqd	⊢ ( 𝜑 → ¬ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 )
38		fveq2	⊢ ( 𝑞 = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) → ( 𝑂 ‘ 𝑞 ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
39	38	fveq1d	⊢ ( 𝑞 = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) )
40	39	eqeq1d	⊢ ( 𝑞 = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 ) )
41	40	elrab	⊢ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ↔ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ dom 𝑂 ∧ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 ) )
42	41	simprbi	⊢ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 )
43	37 42	nsyl	⊢ ( 𝜑 → ¬ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
44		nelne1	⊢ ( ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝑈 ∧ ¬ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) → 𝑈 ≠ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
45	32 43 44	syl2anc	⊢ ( 𝜑 → 𝑈 ≠ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
46	45	necomd	⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ≠ 𝑈 )
47	11 46	eqnetrd	⊢ ( 𝜑 → 𝑄 ≠ 𝑈 )