Theorem minplynzm1p

Description: If a minimal polynomial is nonzero, then it is monic. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	minplynzm1p.b	$$⊢B={\mathrm{Base}}_E$$
	minplynzm1p.z	$$⊢Z=0_{{\mathrm{Poly}}_1\left(E\right)}$$
	minplynzm1p.e	$$⊢\phi \to E\in \mathrm{Field}$$
	minplynzm1p.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	minplynzm1p.m	$$⊢M=E\mathrm{minPoly}F$$
	minplynzm1p.a	$$⊢\phi \to A\in B$$
	minplynzm1p.1	$$⊢\phi \to M\left(A\right)\ne Z$$
	minplynzm1p.u	$$⊢U={Monic}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
Assertion	minplynzm1p	$$⊢\phi \to M\left(A\right)\in U$$

Proof

Step	Hyp	Ref	Expression
1		minplynzm1p.b	$$⊢B={\mathrm{Base}}_E$$
2		minplynzm1p.z	$$⊢Z=0_{{\mathrm{Poly}}_1\left(E\right)}$$
3		minplynzm1p.e	$$⊢\phi \to E\in \mathrm{Field}$$
4		minplynzm1p.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
5		minplynzm1p.m	$$⊢M=E\mathrm{minPoly}F$$
6		minplynzm1p.a	$$⊢\phi \to A\in B$$
7		minplynzm1p.1	$$⊢\phi \to M\left(A\right)\ne Z$$
8		minplynzm1p.u	$$⊢U={Monic}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
9		eqid	$$⊢E{\mathrm{evalSub}}_{1}F=E{\mathrm{evalSub}}_{1}F$$
10		eqid	$$⊢{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
11		eqid	$$⊢0_E=0_E$$
12		eqid	$$⊢\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}=\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}$$
13		eqid	$$⊢\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)$$
14		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
15	9 10 1 3 4 6 11 12 13 14 5	minplyval	$$⊢\phi \to M\left(A\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)$$
16		eqid	$$⊢E{\upharpoonright }_{𝑠}F=E{\upharpoonright }_{𝑠}F$$
17	16	sdrgdrng	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
18	4 17	syl	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
19	3	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
20		sdrgsubrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\in \mathrm{SubRing}\left(E\right)$$
21	4 20	syl	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
22	9 10 1 19 21 6 11 12	ply1annidl	$$⊢\phi \to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)$$
23	15	sneqd	$$⊢\phi \to \left\{M\left(A\right)\right\}=\left\{{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right\}$$
24	23	fveq2d	$$⊢\phi \to \mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{M\left(A\right)\right\}\right)=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right\}\right)$$
25	9 10 1 3 4 6 11 12 13 14	ply1annig1p	$$⊢\phi \to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right\}\right)$$
26	24 25	eqtr4d	$$⊢\phi \to \mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{M\left(A\right)\right\}\right)=\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}$$
27	18	drngringd	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{Ring}$$
28	10	ply1ring	$$⊢E{\upharpoonright }_{𝑠}F\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}$$
29	27 28	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}$$
30	9 10 1 3 4 6 11 12 13 14 5	minplycl	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
31		eqid	$$⊢{\mathrm{Poly}}_1\left(E\right)={\mathrm{Poly}}_1\left(E\right)$$
32		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
33	31 16 10 32 21 2	ressply10g	$$⊢\phi \to Z=0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
34	7 33	neeqtrd	$$⊢\phi \to M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
35		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}=0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
36	32 35 13	pidlnz	$$⊢\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}\wedge M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\wedge M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right)\to \mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{M\left(A\right)\right\}\right)\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
37	29 30 34 36	syl3anc	$$⊢\phi \to \mathrm{RSpan}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\left(\left\{M\left(A\right)\right\}\right)\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
38	26 37	eqnetrrd	$$⊢\phi \to \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}$$
39		eqid	$$⊢\mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)=\mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)$$
40		eqid	$$⊢{\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)={\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
41	10 14 35 39 40 8	ig1pval3	$$⊢\left(E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\wedge \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\right)\wedge \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\ne \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}\right)\to \left({idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\wedge {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in U\wedge {\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)\left({idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right)=inf\left({\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)\left[\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\setminus \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}\right],ℝ,<\right)\right)$$
42	18 22 38 41	syl3anc	$$⊢\phi \to \left({idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in \left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\wedge {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in U\wedge {\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)\left({idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\right)=inf\left({\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)\left[\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\setminus \left\{0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}\right\}\right],ℝ,<\right)\right)$$
43	42	simp2d	$$⊢\phi \to {idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)\left(\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=0_E\right\}\right)\in U$$
44	15 43	eqeltrd	$$⊢\phi \to M\left(A\right)\in U$$