Theorem minplyann

Description: The minimal polynomial for A annihilates A (Contributed by Thierry Arnoux, 25-Apr-2025)

	Ref	Expression
Hypotheses	ply1annig1p.o	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
	ply1annig1p.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
	ply1annig1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	ply1annig1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	ply1annig1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	ply1annig1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	minplyann.1	⊢ 0 = ( 0g ‘ 𝐸 )
	minplyann.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
Assertion	minplyann	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 )

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		minplyann.1	⊢ 0 = ( 0g ‘ 𝐸 )
8		minplyann.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
9		eqid	⊢ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
10		eqid	⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
11		eqid	⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
12	1 2 3 4 5 6 7 9 10 11 8	minplyval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) )
13		eqid	⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
14	13	sdrgdrng	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
15	5 14	syl	⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
16	4	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
17		sdrgsubrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
18	5 17	syl	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
19	1 2 3 16 18 6 7 9	ply1annidl	⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ∈ ( LIdeal ‘ 𝑃 ) )
20		eqid	⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
21	2 11 20	ig1pcl	⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ DivRing ∧ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ∈ ( LIdeal ‘ 𝑃 ) ) → ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
22	15 19 21	syl2anc	⊢ ( 𝜑 → ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
23	12 22	eqeltrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
24		fveq2	⊢ ( 𝑞 = ( 𝑀 ‘ 𝐴 ) → ( 𝑂 ‘ 𝑞 ) = ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) )
25	24	fveq1d	⊢ ( 𝑞 = ( 𝑀 ‘ 𝐴 ) → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) )
26	25	eqeq1d	⊢ ( 𝑞 = ( 𝑀 ‘ 𝐴 ) → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 ) )
27	26	elrab	⊢ ( ( 𝑀 ‘ 𝐴 ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ↔ ( ( 𝑀 ‘ 𝐴 ) ∈ dom 𝑂 ∧ ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 ) )
28	23 27	sylib	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ∈ dom 𝑂 ∧ ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 ) )
29	28	simprd	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 )