Theorem minplymindeg

Description: The minimal polynomial of A is minimal among the nonzero annihilators of A with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-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$$
	minplymindeg.0	$$⊢\underset{\dot{}}{0}=0_E$$
	minplymindeg.m	$$⊢M=E\mathrm{minPoly}F$$
	minplymindeg.d	$$⊢D={\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
	minplymindeg.z	$$⊢Z=0_P$$
	minplymindeg.u	$$⊢U={\mathrm{Base}}_P$$
	minplymindeg.1	$$⊢\phi \to O\left(H\right)\left(A\right)=\underset{\dot{}}{0}$$
	minplymindeg.h	$$⊢\phi \to H\in U$$
	minplymindeg.2	$$⊢\phi \to H\ne Z$$
Assertion	minplymindeg	$$⊢\phi \to D\left(M\left(A\right)\right)\le D\left(H\right)$$

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		minplymindeg.0	$$⊢\underset{\dot{}}{0}=0_E$$
8		minplymindeg.m	$$⊢M=E\mathrm{minPoly}F$$
9		minplymindeg.d	$$⊢D={\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
10		minplymindeg.z	$$⊢Z=0_P$$
11		minplymindeg.u	$$⊢U={\mathrm{Base}}_P$$
12		minplymindeg.1	$$⊢\phi \to O\left(H\right)\left(A\right)=\underset{\dot{}}{0}$$
13		minplymindeg.h	$$⊢\phi \to H\in U$$
14		minplymindeg.2	$$⊢\phi \to H\ne Z$$
15		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\}$$
16		eqid	$$⊢\mathrm{RSpan}\left(P\right)=\mathrm{RSpan}\left(P\right)$$
17		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
18	1 2 3 4 5 6 7 15 16 17 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)$$
19	18	fveq2d	$$⊢\phi \to D\left(M\left(A\right)\right)=D\left({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)\right)$$
20		eqid	$$⊢E{\upharpoonright }_{𝑠}F=E{\upharpoonright }_{𝑠}F$$
21	20	sdrgdrng	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
22	5 21	syl	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
23	4	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
24		sdrgsubrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\in \mathrm{SubRing}\left(E\right)$$
25	5 24	syl	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
26	1 2 3 23 25 6 7 15	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)$$
27		fveq2	$$⊢q=H\to O\left(q\right)=O\left(H\right)$$
28	27	fveq1d	$$⊢q=H\to O\left(q\right)\left(A\right)=O\left(H\right)\left(A\right)$$
29	28	eqeq1d	$$⊢q=H\to \left(O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\leftrightarrow O\left(H\right)\left(A\right)=\underset{\dot{}}{0}\right)$$
30	1 2 11 23 25	evls1dm	$$⊢\phi \to \mathrm{dom}O=U$$
31	13 30	eleqtrrd	$$⊢\phi \to H\in \mathrm{dom}O$$
32	29 31 12	elrabd	$$⊢\phi \to H\in \left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
33	2 17 11 22 26 9 10 32 14	ig1pmindeg	$$⊢\phi \to D\left({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)\right)\le D\left(H\right)$$
34	19 33	eqbrtrd	$$⊢\phi \to D\left(M\left(A\right)\right)\le D\left(H\right)$$