Theorem minplyann

Description: The minimal polynomial for A annihilates A . (Contributed by Thierry Arnoux, 25-Apr-2025)

	Ref	Expression
Hypotheses	ply1annig1p.o	$$⊢O=E{\mathrm{evalSub}}_{1}F$$
	ply1annig1p.p	$$⊢P={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
	ply1annig1p.b	$$⊢B={\mathrm{Base}}_E$$
	ply1annig1p.e	$$⊢\phi \to E\in \mathrm{Field}$$
	ply1annig1p.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	ply1annig1p.a	$$⊢\phi \to A\in B$$
	minplyann.1	$$⊢\underset{\dot{}}{0}=0_E$$
	minplyann.m	$$⊢M=E\mathrm{minPoly}F$$
Assertion	minplyann	$$⊢\phi \to O\left(M\left(A\right)\right)\left(A\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		ply1annig1p.o	$$⊢O=E{\mathrm{evalSub}}_{1}F$$
2		ply1annig1p.p	$$⊢P={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
3		ply1annig1p.b	$$⊢B={\mathrm{Base}}_E$$
4		ply1annig1p.e	$$⊢\phi \to E\in \mathrm{Field}$$
5		ply1annig1p.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
6		ply1annig1p.a	$$⊢\phi \to A\in B$$
7		minplyann.1	$$⊢\underset{\dot{}}{0}=0_E$$
8		minplyann.m	$$⊢M=E\mathrm{minPoly}F$$
9		eqid	$$⊢\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
10		eqid	$$⊢\mathrm{RSpan}\left(P\right)=\mathrm{RSpan}\left(P\right)$$
11		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
12	1 2 3 4 5 6 7 9 10 11 8	minplyval	$$⊢\phi \to M\left(A\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}\right)$$
13		eqid	$$⊢E{\upharpoonright }_{𝑠}F=E{\upharpoonright }_{𝑠}F$$
14	13	sdrgdrng	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
15	5 14	syl	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
16	4	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
17		sdrgsubrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\in \mathrm{SubRing}\left(E\right)$$
18	5 17	syl	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
19	1 2 3 16 18 6 7 9	ply1annidl	$$⊢\phi \to \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(P\right)$$
20		eqid	$$⊢\mathrm{LIdeal}\left(P\right)=\mathrm{LIdeal}\left(P\right)$$
21	2 11 20	ig1pcl	$$⊢\left(E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\wedge \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(P\right)\right)\to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}\right)\in \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
22	15 19 21	syl2anc	$$⊢\phi \to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}\right)\in \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
23	12 22	eqeltrd	$$⊢\phi \to M\left(A\right)\in \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
24		fveq2	$$⊢q=M\left(A\right)\to O\left(q\right)=O\left(M\left(A\right)\right)$$
25	24	fveq1d	$$⊢q=M\left(A\right)\to O\left(q\right)\left(A\right)=O\left(M\left(A\right)\right)\left(A\right)$$
26	25	eqeq1d	$$⊢q=M\left(A\right)\to \left(O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\leftrightarrow O\left(M\left(A\right)\right)\left(A\right)=\underset{\dot{}}{0}\right)$$
27	26	elrab	$$⊢M\left(A\right)\in \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}\leftrightarrow \left(M\left(A\right)\in \mathrm{dom}O\wedge O\left(M\left(A\right)\right)\left(A\right)=\underset{\dot{}}{0}\right)$$
28	23 27	sylib	$$⊢\phi \to \left(M\left(A\right)\in \mathrm{dom}O\wedge O\left(M\left(A\right)\right)\left(A\right)=\underset{\dot{}}{0}\right)$$
29	28	simprd	$$⊢\phi \to O\left(M\left(A\right)\right)\left(A\right)=\underset{\dot{}}{0}$$