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{\mathrm{evalSub}}_{1}S$$
	ply1annidl.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
	ply1annidl.b	$$⊢B={\mathrm{Base}}_R$$
	ply1annidl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	ply1annidl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	ply1annidl.a	$$⊢\phi \to A\in B$$
	ply1annidl.0	$$⊢\underset{\dot{}}{0}=0_R$$
	ply1annidl.q	$$⊢Q=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
Assertion	ply1annidl	$$⊢\phi \to Q\in \mathrm{LIdeal}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1annidl.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
2		ply1annidl.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
3		ply1annidl.b	$$⊢B={\mathrm{Base}}_R$$
4		ply1annidl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
5		ply1annidl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
6		ply1annidl.a	$$⊢\phi \to A\in B$$
7		ply1annidl.0	$$⊢\underset{\dot{}}{0}=0_R$$
8		ply1annidl.q	$$⊢Q=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
9		eqid	$$⊢\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)=\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)$$
10	1 2 3 4 5 6 7 8 9	ply1annidllem	$$⊢\phi \to Q={\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
11		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
12	1 2 3 11 4 5 6 9	evls1maprhm	$$⊢\phi \to \left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)\in \left(P\mathrm{RingHom}R\right)$$
13	4	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
14		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
15	14 7	lidl0	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)$$
16	13 15	syl	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)$$
17		eqid	$$⊢\mathrm{LIdeal}\left(P\right)=\mathrm{LIdeal}\left(P\right)$$
18	17	rhmpreimaidl	$$⊢\left(\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)\in \left(P\mathrm{RingHom}R\right)\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)\right)\to {\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LIdeal}\left(P\right)$$
19	12 16 18	syl2anc	$$⊢\phi \to {\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LIdeal}\left(P\right)$$
20	10 19	eqeltrd	$$⊢\phi \to Q\in \mathrm{LIdeal}\left(P\right)$$