Theorem minplycl

Description: The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-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$$
	ply1annig1p.0	$$⊢\underset{\dot{}}{0}=0_E$$
	ply1annig1p.q	$$⊢Q=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
	ply1annig1p.k	$$⊢K=\mathrm{RSpan}\left(P\right)$$
	ply1annig1p.g	$$⊢G={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
	minplyval.1	No typesetting found for |- M = ( E minPoly F ) with typecode |-
Assertion	minplycl	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_P$$

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		ply1annig1p.0	$$⊢\underset{\dot{}}{0}=0_E$$
8		ply1annig1p.q	$$⊢Q=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
9		ply1annig1p.k	$$⊢K=\mathrm{RSpan}\left(P\right)$$
10		ply1annig1p.g	$$⊢G={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
11		minplyval.1	Could not format M = ( E minPoly F ) : No typesetting found for |- M = ( E minPoly F ) with typecode |-
12	1 2 3 4 5 6 7 8 9 10 11	minplyval	$$⊢\phi \to M\left(A\right)=G\left(Q\right)$$
13	4	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
14		issdrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\leftrightarrow \left(E\in \mathrm{DivRing}\wedge F\in \mathrm{SubRing}\left(E\right)\wedge E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\right)$$
15	5 14	sylib	$$⊢\phi \to \left(E\in \mathrm{DivRing}\wedge F\in \mathrm{SubRing}\left(E\right)\wedge E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\right)$$
16	15	simp2d	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
17	1 2 3 13 16 6 7 8	ply1annidl	$$⊢\phi \to Q\in \mathrm{LIdeal}\left(P\right)$$
18		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
19		eqid	$$⊢\mathrm{LIdeal}\left(P\right)=\mathrm{LIdeal}\left(P\right)$$
20	18 19	lidlss	$$⊢Q\in \mathrm{LIdeal}\left(P\right)\to Q\subseteq {\mathrm{Base}}_P$$
21	17 20	syl	$$⊢\phi \to Q\subseteq {\mathrm{Base}}_P$$
22	15	simp3d	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
23	2 10 19	ig1pcl	$$⊢\left(E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\wedge Q\in \mathrm{LIdeal}\left(P\right)\right)\to G\left(Q\right)\in Q$$
24	22 17 23	syl2anc	$$⊢\phi \to G\left(Q\right)\in Q$$
25	21 24	sseldd	$$⊢\phi \to G\left(Q\right)\in {\mathrm{Base}}_P$$
26	12 25	eqeltrd	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_P$$