Theorem minplym1p

Description: A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	irngnminplynz.z	$$⊢Z=0_{{\mathrm{Poly}}_1\left(E\right)}$$
	irngnminplynz.e	$$⊢\phi \to E\in \mathrm{Field}$$
	irngnminplynz.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	irngnminplynz.m	No typesetting found for |- M = ( E minPoly F ) with typecode |-
	irngnminplynz.a	$$⊢\phi \to A\in \left(E\mathrm{IntgRing}F\right)$$
	minplym1p.1	$$⊢U={Monic}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
Assertion	minplym1p	$$⊢\phi \to M\left(A\right)\in U$$

Proof

Step	Hyp	Ref	Expression
1		irngnminplynz.z	$$⊢Z=0_{{\mathrm{Poly}}_1\left(E\right)}$$
2		irngnminplynz.e	$$⊢\phi \to E\in \mathrm{Field}$$
3		irngnminplynz.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
4		irngnminplynz.m	Could not format M = ( E minPoly F ) : No typesetting found for |- M = ( E minPoly F ) with typecode |-
5		irngnminplynz.a	$$⊢\phi \to A\in \left(E\mathrm{IntgRing}F\right)$$
6		minplym1p.1	$$⊢U={Monic}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
7		eqid	$$⊢E{\mathrm{evalSub}}_{1}F=E{\mathrm{evalSub}}_{1}F$$
8		eqid	$$⊢{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
9		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
10		eqid	$$⊢E{\upharpoonright }_{𝑠}F=E{\upharpoonright }_{𝑠}F$$
11		eqid	$$⊢0_E=0_E$$
12	2	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
13		sdrgsubrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\in \mathrm{SubRing}\left(E\right)$$
14	3 13	syl	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
15	7 10 9 11 12 14	irngssv	$$⊢\phi \to E\mathrm{IntgRing}F\subseteq {\mathrm{Base}}_E$$
16	15 5	sseldd	$$⊢\phi \to A\in {\mathrm{Base}}_E$$
17		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\}$$
18		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)$$
19		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
20	7 8 9 2 3 16 11 17 18 19 4	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)$$
21	10	sdrgdrng	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
22	3 21	syl	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
23	7 8 9 12 14 16 11 17	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)$$
24	20	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\}$$
25	24	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)$$
26	7 8 9 2 3 16 11 17 18 19	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)$$
27	25 26	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\}$$
28	22	drngringd	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{Ring}$$
29	8	ply1ring	$$⊢E{\upharpoonright }_{𝑠}F\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}$$
30	28 29	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)\in \mathrm{Ring}$$
31	7 8 9 2 3 16 11 17 18 19 4	minplycl	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
32	1 2 3 4 5	irngnminplynz	$$⊢\phi \to M\left(A\right)\ne Z$$
33		eqid	$$⊢{\mathrm{Poly}}_1\left(E\right)={\mathrm{Poly}}_1\left(E\right)$$
34		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
35	33 10 8 34 14 1	ressply10g	$$⊢\phi \to Z=0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
36	32 35	neeqtrd	$$⊢\phi \to M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
37		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}=0_{{\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)}$$
38	34 37 18	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\}$$
39	30 31 36 38	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\}$$
40	27 39	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\}$$
41		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)$$
42		eqid	$$⊢{\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)={\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
43	8 19 37 41 42 6	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)=sup\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)$$
44	22 23 40 43	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)=sup\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)$$
45	44	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$$
46	20 45	eqeltrd	$$⊢\phi \to M\left(A\right)\in U$$