Theorem ply1annidl

Description: The set Q of polynomials annihilating an element A forms an ideal. (Contributed by Thierry Arnoux, 9-Feb-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. }
Assertion	ply1annidl	|- ( ph -> Q e. ( LIdeal ` P ) )

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		eqid	|- ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) = ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) )
10	1 2 3 4 5 6 7 8 9	ply1annidllem	|- ( ph -> Q = ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) )
11		eqid	|- ( Base ` P ) = ( Base ` P )
12	1 2 3 11 4 5 6 9	evls1maprhm	|- ( ph -> ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom R ) )
13	4	crngringd	|- ( ph -> R e. Ring )
14		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
15	14 7	lidl0	|- ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
16	13 15	syl	|- ( ph -> { .0. } e. ( LIdeal ` R ) )
17		eqid	|- ( LIdeal ` P ) = ( LIdeal ` P )
18	17	rhmpreimaidl	|- ( ( ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom R ) /\ { .0. } e. ( LIdeal ` R ) ) -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( LIdeal ` P ) )
19	12 16 18	syl2anc	|- ( ph -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( LIdeal ` P ) )
20	10 19	eqeltrd	|- ( ph -> Q e. ( LIdeal ` P ) )