Theorem minplymindeg

Description: The minimal polynomial of A is minimal among the nonzero annihilators of A with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	ply1annig1p.o	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
	ply1annig1p.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
	ply1annig1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	ply1annig1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	ply1annig1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	ply1annig1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	minplymindeg.0	⊢ 0 = ( 0g ‘ 𝐸 )
	minplymindeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	minplymindeg.d	⊢ 𝐷 = ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) )
	minplymindeg.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
	minplymindeg.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	minplymindeg.1	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) = 0 )
	minplymindeg.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑈 )
	minplymindeg.2	⊢ ( 𝜑 → 𝐻 ≠ 𝑍 )
Assertion	minplymindeg	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ≤ ( 𝐷 ‘ 𝐻 ) )

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		minplymindeg.0	⊢ 0 = ( 0g ‘ 𝐸 )
8		minplymindeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
9		minplymindeg.d	⊢ 𝐷 = ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) )
10		minplymindeg.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
11		minplymindeg.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
12		minplymindeg.1	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) = 0 )
13		minplymindeg.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑈 )
14		minplymindeg.2	⊢ ( 𝜑 → 𝐻 ≠ 𝑍 )
15		eqid	⊢ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
16		eqid	⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
17		eqid	⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
18	1 2 3 4 5 6 7 15 16 17 8	minplyval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) )
19	18	fveq2d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝐷 ‘ ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ) )
20		eqid	⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
21	20	sdrgdrng	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
22	5 21	syl	⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
23	4	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
24		sdrgsubrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
25	5 24	syl	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
26	1 2 3 23 25 6 7 15	ply1annidl	⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ∈ ( LIdeal ‘ 𝑃 ) )
27		fveq2	⊢ ( 𝑞 = 𝐻 → ( 𝑂 ‘ 𝑞 ) = ( 𝑂 ‘ 𝐻 ) )
28	27	fveq1d	⊢ ( 𝑞 = 𝐻 → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) )
29	28	eqeq1d	⊢ ( 𝑞 = 𝐻 → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) = 0 ) )
30	1 2 11 23 25	evls1dm	⊢ ( 𝜑 → dom 𝑂 = 𝑈 )
31	13 30	eleqtrrd	⊢ ( 𝜑 → 𝐻 ∈ dom 𝑂 )
32	29 31 12	elrabd	⊢ ( 𝜑 → 𝐻 ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
33	2 17 11 22 26 9 10 32 14	ig1pmindeg	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ) ≤ ( 𝐷 ‘ 𝐻 ) )
34	19 33	eqbrtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ≤ ( 𝐷 ‘ 𝐻 ) )