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	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
	ply1annig1p.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
	ply1annig1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	ply1annig1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	ply1annig1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	ply1annig1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	ply1annig1p.0	⊢ 0 = ( 0g ‘ 𝐸 )
	ply1annig1p.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
	ply1annig1p.k	⊢ 𝐾 = ( RSpan ‘ 𝑃 )
	ply1annig1p.g	⊢ 𝐺 = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
	minplyval.1	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
Assertion	minplyval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1annig1p.o	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
2		ply1annig1p.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
3		ply1annig1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
4		ply1annig1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
5		ply1annig1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
6		ply1annig1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		ply1annig1p.0	⊢ 0 = ( 0g ‘ 𝐸 )
8		ply1annig1p.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9		ply1annig1p.k	⊢ 𝐾 = ( RSpan ‘ 𝑃 )
10		ply1annig1p.g	⊢ 𝐺 = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
11		minplyval.1	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
12	4	elexd	⊢ ( 𝜑 → 𝐸 ∈ V )
13	5	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
14	3	fvexi	⊢ 𝐵 ∈ V
15	14	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
16	15	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) ∈ V )
17		fveq2	⊢ ( 𝑒 = 𝐸 → ( Base ‘ 𝑒 ) = ( Base ‘ 𝐸 ) )
18	17 3	eqtr4di	⊢ ( 𝑒 = 𝐸 → ( Base ‘ 𝑒 ) = 𝐵 )
19	18	adantr	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑒 ) = 𝐵 )
20		oveq12	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 ↾s 𝑓 ) = ( 𝐸 ↾s 𝐹 ) )
21	20	fveq2d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) )
22	21 10	eqtr4di	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) = 𝐺 )
23		oveq12	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 evalSub1 𝑓 ) = ( 𝐸 evalSub1 𝐹 ) )
24	23 1	eqtr4di	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 evalSub1 𝑓 ) = 𝑂 )
25	24	dmeqd	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → dom ( 𝑒 evalSub1 𝑓 ) = dom 𝑂 )
26	24	fveq1d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) = ( 𝑂 ‘ 𝑞 ) )
27	26	fveq1d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) )
28		fveq2	⊢ ( 𝑒 = 𝐸 → ( 0g ‘ 𝑒 ) = ( 0g ‘ 𝐸 ) )
29	28	adantr	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 0g ‘ 𝑒 ) = ( 0g ‘ 𝐸 ) )
30	29 7	eqtr4di	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 0g ‘ 𝑒 ) = 0 )
31	27 30	eqeq12d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) ↔ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 ) )
32	25 31	rabeqbidv	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } )
33	22 32	fveq12d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) = ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) )
34	19 33	mpteq12dv	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
35		df-minply	⊢ minPoly = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) ) )
36	34 35	ovmpoga	⊢ ( ( 𝐸 ∈ V ∧ 𝐹 ∈ V ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) ∈ V ) → ( 𝐸 minPoly 𝐹 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
37	12 13 16 36	syl3anc	⊢ ( 𝜑 → ( 𝐸 minPoly 𝐹 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
38	11 37	eqtrid	⊢ ( 𝜑 → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
39		fveqeq2	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ) )
40	39	rabbidv	⊢ ( 𝑥 = 𝐴 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
41	40 8	eqtr4di	⊢ ( 𝑥 = 𝐴 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } = 𝑄 )
42	41	fveq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) = ( 𝐺 ‘ 𝑄 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) = ( 𝐺 ‘ 𝑄 ) )
44		fvexd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑄 ) ∈ V )
45	38 43 6 44	fvmptd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑄 ) )