Theorem ply1annidllem

Description: Write the set Q of polynomials annihilating an element A as the kernel of the ring homomorphism F mapping polynomials p to their subring evaluation at a given point A . (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\}$$
	ply1annidllem.f	$$⊢F=\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)$$
Assertion	ply1annidllem	$$⊢\phi \to Q=F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\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		ply1annidllem.f	$$⊢F=\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)$$
10		nfv	$$⊢Ⅎp\phi$$
11		fvexd	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_P\right)\to O\left(p\right)\left(A\right)\in \mathrm{V}$$
12	10 11 9	fnmptd	$$⊢\phi \to FFn{\mathrm{Base}}_P$$
13		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
14	1 2 13 4 5	evls1fn	$$⊢\phi \to OFn{\mathrm{Base}}_P$$
15	14	fndmd	$$⊢\phi \to \mathrm{dom}O={\mathrm{Base}}_P$$
16	15	fneq2d	$$⊢\phi \to \left(FFn\mathrm{dom}O\leftrightarrow FFn{\mathrm{Base}}_P\right)$$
17	12 16	mpbird	$$⊢\phi \to FFn\mathrm{dom}O$$
18		fniniseg2	$$⊢FFn\mathrm{dom}O\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{q\in \mathrm{dom}O|F\left(q\right)=\underset{\dot{}}{0}\right\}$$
19	17 18	syl	$$⊢\phi \to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{q\in \mathrm{dom}O|F\left(q\right)=\underset{\dot{}}{0}\right\}$$
20		fveq2	$$⊢p=q\to O\left(p\right)=O\left(q\right)$$
21	20	fveq1d	$$⊢p=q\to O\left(p\right)\left(A\right)=O\left(q\right)\left(A\right)$$
22	15	eleq2d	$$⊢\phi \to \left(q\in \mathrm{dom}O\leftrightarrow q\in {\mathrm{Base}}_P\right)$$
23	22	biimpa	$$⊢\left(\phi \wedge q\in \mathrm{dom}O\right)\to q\in {\mathrm{Base}}_P$$
24		fvexd	$$⊢\left(\phi \wedge q\in \mathrm{dom}O\right)\to O\left(q\right)\left(A\right)\in \mathrm{V}$$
25	9 21 23 24	fvmptd3	$$⊢\left(\phi \wedge q\in \mathrm{dom}O\right)\to F\left(q\right)=O\left(q\right)\left(A\right)$$
26	25	eqeq1d	$$⊢\left(\phi \wedge q\in \mathrm{dom}O\right)\to \left(F\left(q\right)=\underset{\dot{}}{0}\leftrightarrow O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right)$$
27	26	rabbidva	$$⊢\phi \to \left\{q\in \mathrm{dom}O|F\left(q\right)=\underset{\dot{}}{0}\right\}=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
28	19 27	eqtr2d	$$⊢\phi \to \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}=F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
29	8 28	eqtrid	$$⊢\phi \to Q=F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$