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	\|- O = ( R evalSub1 S )
	ply1annidl.p	\|- P = ( Poly1 ` ( R \|`s S ) )
	ply1annidl.b	\|- B = ( Base ` R )
	ply1annidl.r	\|- ( ph -> R e. CRing )
	ply1annidl.s	\|- ( ph -> S e. ( SubRing ` R ) )
	ply1annidl.a	\|- ( ph -> A e. B )
	ply1annidl.0	\|- .0. = ( 0g ` R )
	ply1annidl.q	\|- Q = { q e. dom O \| ( ( O ` q ) ` A ) = .0. }
	ply1annnr.u	\|- U = ( Base ` P )
	ply1annnr.1	\|- ( ph -> R e. NzRing )
Assertion	ply1annnr	\|- ( ph -> Q =/= U )

Proof

Step	Hyp	Ref	Expression
1		ply1annidl.o	\|- O = ( R evalSub1 S )
2		ply1annidl.p	\|- P = ( Poly1 ` ( R \|`s S ) )
3		ply1annidl.b	\|- B = ( Base ` R )
4		ply1annidl.r	\|- ( ph -> R e. CRing )
5		ply1annidl.s	\|- ( ph -> S e. ( SubRing ` R ) )
6		ply1annidl.a	\|- ( ph -> A e. B )
7		ply1annidl.0	\|- .0. = ( 0g ` R )
8		ply1annidl.q	\|- Q = { q e. dom O \| ( ( O ` q ) ` A ) = .0. }
9		ply1annnr.u	\|- U = ( Base ` P )
10		ply1annnr.1	\|- ( ph -> R e. NzRing )
11	8	a1i	\|- ( ph -> Q = { q e. dom O \| ( ( O ` q ) ` A ) = .0. } )
12	4	crngringd	\|- ( ph -> R e. Ring )
13		eqid	\|- ( 1r ` R ) = ( 1r ` R )
14	13	subrg1cl	\|- ( S e. ( SubRing ` R ) -> ( 1r ` R ) e. S )
15	5 14	syl	\|- ( ph -> ( 1r ` R ) e. S )
16	3	subrgss	\|- ( S e. ( SubRing ` R ) -> S C_ B )
17	5 16	syl	\|- ( ph -> S C_ B )
18		eqid	\|- ( R \|`s S ) = ( R \|`s S )
19	18 3 13	ress1r	\|- ( ( R e. Ring /\ ( 1r ` R ) e. S /\ S C_ B ) -> ( 1r ` R ) = ( 1r ` ( R \|`s S ) ) )
20	12 15 17 19	syl3anc	\|- ( ph -> ( 1r ` R ) = ( 1r ` ( R \|`s S ) ) )
21	20	fveq2d	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( algSc ` P ) ` ( 1r ` ( R \|`s S ) ) ) )
22		eqid	\|- ( algSc ` P ) = ( algSc ` P )
23		eqid	\|- ( 1r ` ( R \|`s S ) ) = ( 1r ` ( R \|`s S ) )
24		eqid	\|- ( 1r ` P ) = ( 1r ` P )
25	18	subrgring	\|- ( S e. ( SubRing ` R ) -> ( R \|`s S ) e. Ring )
26	5 25	syl	\|- ( ph -> ( R \|`s S ) e. Ring )
27	2 22 23 24 26	ply1ascl1	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` ( R \|`s S ) ) ) = ( 1r ` P ) )
28	21 27	eqtrd	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
29	2	ply1ring	\|- ( ( R \|`s S ) e. Ring -> P e. Ring )
30	9 24	ringidcl	\|- ( P e. Ring -> ( 1r ` P ) e. U )
31	26 29 30	3syl	\|- ( ph -> ( 1r ` P ) e. U )
32	28 31	eqeltrd	\|- ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. U )
33	1 2 18 3 22 4 5 15 6	evls1scafv	\|- ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = ( 1r ` R ) )
34	13 7	nzrnz	\|- ( R e. NzRing -> ( 1r ` R ) =/= .0. )
35	10 34	syl	\|- ( ph -> ( 1r ` R ) =/= .0. )
36	33 35	eqnetrd	\|- ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) =/= .0. )
37	36	neneqd	\|- ( ph -> -. ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. )
38		fveq2	\|- ( q = ( ( algSc ` P ) ` ( 1r ` R ) ) -> ( O ` q ) = ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
39	38	fveq1d	\|- ( q = ( ( algSc ` P ) ` ( 1r ` R ) ) -> ( ( O ` q ) ` A ) = ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) )
40	39	eqeq1d	\|- ( q = ( ( algSc ` P ) ` ( 1r ` R ) ) -> ( ( ( O ` q ) ` A ) = .0. <-> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. ) )
41	40	elrab	\|- ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O \| ( ( O ` q ) ` A ) = .0. } <-> ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. dom O /\ ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. ) )
42	41	simprbi	\|- ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O \| ( ( O ` q ) ` A ) = .0. } -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. )
43	37 42	nsyl	\|- ( ph -> -. ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O \| ( ( O ` q ) ` A ) = .0. } )
44		nelne1	\|- ( ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. U /\ -. ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O \| ( ( O ` q ) ` A ) = .0. } ) -> U =/= { q e. dom O \| ( ( O ` q ) ` A ) = .0. } )
45	32 43 44	syl2anc	\|- ( ph -> U =/= { q e. dom O \| ( ( O ` q ) ` A ) = .0. } )
46	45	necomd	\|- ( ph -> { q e. dom O \| ( ( O ` q ) ` A ) = .0. } =/= U )
47	11 46	eqnetrd	\|- ( ph -> Q =/= U )

Metamath Proof Explorer

Theorem ply1annnr

Proof