Theorem minplyval

Description: Expand the value of the minimal polynomial ( MA ) for a given element A . It is defined as the unique monic polynomial of minimal degree which annihilates A . By ply1annig1p , that polynomial generates the ideal of the annihilators of A . (Contributed by Thierry Arnoux, 9-Feb-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	minplyval	$$⊢\phi \to M\left(A\right)=G\left(Q\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		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	4	elexd	$$⊢\phi \to E\in \mathrm{V}$$
13	5	elexd	$$⊢\phi \to F\in \mathrm{V}$$
14	3	fvexi	$$⊢B\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to B\in \mathrm{V}$$
16	15	mptexd	$$⊢\phi \to \left(x\in B⟼G\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}\right)\right)\in \mathrm{V}$$
17		fveq2	$$⊢e=E\to {\mathrm{Base}}_e={\mathrm{Base}}_E$$
18	17 3	eqtr4di	$$⊢e=E\to {\mathrm{Base}}_e=B$$
19	18	adantr	$$⊢\left(e=E\wedge f=F\right)\to {\mathrm{Base}}_e=B$$
20		oveq12	$$⊢\left(e=E\wedge f=F\right)\to e{\upharpoonright }_{𝑠}f=E{\upharpoonright }_{𝑠}F$$
21	20	fveq2d	$$⊢\left(e=E\wedge f=F\right)\to {idlGen}_{\mathrm{1p}}\left(e{\upharpoonright }_{𝑠}f\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
22	21 10	eqtr4di	$$⊢\left(e=E\wedge f=F\right)\to {idlGen}_{\mathrm{1p}}\left(e{\upharpoonright }_{𝑠}f\right)=G$$
23		oveq12	$$⊢\left(e=E\wedge f=F\right)\to e{\mathrm{evalSub}}_{1}f=E{\mathrm{evalSub}}_{1}F$$
24	23 1	eqtr4di	$$⊢\left(e=E\wedge f=F\right)\to e{\mathrm{evalSub}}_{1}f=O$$
25	24	dmeqd	$$⊢\left(e=E\wedge f=F\right)\to \mathrm{dom}\left(e{\mathrm{evalSub}}_{1}f\right)=\mathrm{dom}O$$
26	24	fveq1d	$$⊢\left(e=E\wedge f=F\right)\to \left(e{\mathrm{evalSub}}_{1}f\right)\left(q\right)=O\left(q\right)$$
27	26	fveq1d	$$⊢\left(e=E\wedge f=F\right)\to \left(e{\mathrm{evalSub}}_{1}f\right)\left(q\right)\left(x\right)=O\left(q\right)\left(x\right)$$
28		fveq2	$$⊢e=E\to 0_e=0_E$$
29	28	adantr	$$⊢\left(e=E\wedge f=F\right)\to 0_e=0_E$$
30	29 7	eqtr4di	$$⊢\left(e=E\wedge f=F\right)\to 0_e=\underset{\dot{}}{0}$$
31	27 30	eqeq12d	$$⊢\left(e=E\wedge f=F\right)\to \left(\left(e{\mathrm{evalSub}}_{1}f\right)\left(q\right)\left(x\right)=0_e\leftrightarrow O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
32	25 31	rabeqbidv	$$⊢\left(e=E\wedge f=F\right)\to \left\{q\in \mathrm{dom}\left(e{\mathrm{evalSub}}_{1}f\right)|\left(e{\mathrm{evalSub}}_{1}f\right)\left(q\right)\left(x\right)=0_e\right\}=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}$$
33	22 32	fveq12d	$$⊢\left(e=E\wedge f=F\right)\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(x\right)=0_e\right\}\right)=G\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}\right)$$
34	19 33	mpteq12dv	$$⊢\left(e=E\wedge f=F\right)\to \left(x\in {\mathrm{Base}}_e⟼{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(x\right)=0_e\right\}\right)\right)=\left(x\in B⟼G\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}\right)\right)$$
35		df-minply	Could not format minPoly = ( e e. _V , f e. _V |-> ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { q e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` q ) ` x ) = ( 0g ` e ) } ) ) ) : No typesetting found for |- minPoly = ( e e. _V , f e. _V |-> ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { q e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` q ) ` x ) = ( 0g ` e ) } ) ) ) with typecode |-
36	34 35	ovmpoga	Could not format ( ( E e. _V /\ F e. _V /\ ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) e. _V ) -> ( E minPoly F ) = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) ) : No typesetting found for |- ( ( E e. _V /\ F e. _V /\ ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) e. _V ) -> ( E minPoly F ) = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) ) with typecode |-
37	12 13 16 36	syl3anc	Could not format ( ph -> ( E minPoly F ) = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) ) : No typesetting found for |- ( ph -> ( E minPoly F ) = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) ) with typecode |-
38	11 37	eqtrid	$$⊢\phi \to M=\left(x\in B⟼G\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}\right)\right)$$
39		fveqeq2	$$⊢x=A\to \left(O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\leftrightarrow O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right)$$
40	39	rabbidv	$$⊢x=A\to \left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
41	40 8	eqtr4di	$$⊢x=A\to \left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}=Q$$
42	41	fveq2d	$$⊢x=A\to G\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}\right)=G\left(Q\right)$$
43	42	adantl	$$⊢\left(\phi \wedge x=A\right)\to G\left(\left\{q\in \mathrm{dom}O|O\left(q\right)\left(x\right)=\underset{\dot{}}{0}\right\}\right)=G\left(Q\right)$$
44		fvexd	$$⊢\phi \to G\left(Q\right)\in \mathrm{V}$$
45	38 43 6 44	fvmptd	$$⊢\phi \to M\left(A\right)=G\left(Q\right)$$