Theorem minplyann

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

	Ref	Expression
Hypotheses	ply1annig1p.o	|- O = ( E evalSub1 F )
	ply1annig1p.p	|- P = ( Poly1 ` ( E |`s F ) )
	ply1annig1p.b	|- B = ( Base ` E )
	ply1annig1p.e	|- ( ph -> E e. Field )
	ply1annig1p.f	|- ( ph -> F e. ( SubDRing ` E ) )
	ply1annig1p.a	|- ( ph -> A e. B )
	minplyann.1	|- .0. = ( 0g ` E )
	minplyann.m	|- M = ( E minPoly F )
Assertion	minplyann	|- ( ph -> ( ( O ` ( M ` A ) ) ` A ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		ply1annig1p.o	|- O = ( E evalSub1 F )
2		ply1annig1p.p	|- P = ( Poly1 ` ( E |`s F ) )
3		ply1annig1p.b	|- B = ( Base ` E )
4		ply1annig1p.e	|- ( ph -> E e. Field )
5		ply1annig1p.f	|- ( ph -> F e. ( SubDRing ` E ) )
6		ply1annig1p.a	|- ( ph -> A e. B )
7		minplyann.1	|- .0. = ( 0g ` E )
8		minplyann.m	|- M = ( E minPoly F )
9		eqid	|- { q e. dom O | ( ( O ` q ) ` A ) = .0. } = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
10		eqid	|- ( RSpan ` P ) = ( RSpan ` P )
11		eqid	|- ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
12	1 2 3 4 5 6 7 9 10 11 8	minplyval	|- ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) )
13		eqid	|- ( E |`s F ) = ( E |`s F )
14	13	sdrgdrng	|- ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
15	5 14	syl	|- ( ph -> ( E |`s F ) e. DivRing )
16	4	fldcrngd	|- ( ph -> E e. CRing )
17		sdrgsubrg	|- ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
18	5 17	syl	|- ( ph -> F e. ( SubRing ` E ) )
19	1 2 3 16 18 6 7 9	ply1annidl	|- ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = .0. } e. ( LIdeal ` P ) )
20		eqid	|- ( LIdeal ` P ) = ( LIdeal ` P )
21	2 11 20	ig1pcl	|- ( ( ( E |`s F ) e. DivRing /\ { q e. dom O | ( ( O ` q ) ` A ) = .0. } e. ( LIdeal ` P ) ) -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
22	15 19 21	syl2anc	|- ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
23	12 22	eqeltrd	|- ( ph -> ( M ` A ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
24		fveq2	|- ( q = ( M ` A ) -> ( O ` q ) = ( O ` ( M ` A ) ) )
25	24	fveq1d	|- ( q = ( M ` A ) -> ( ( O ` q ) ` A ) = ( ( O ` ( M ` A ) ) ` A ) )
26	25	eqeq1d	|- ( q = ( M ` A ) -> ( ( ( O ` q ) ` A ) = .0. <-> ( ( O ` ( M ` A ) ) ` A ) = .0. ) )
27	26	elrab	|- ( ( M ` A ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } <-> ( ( M ` A ) e. dom O /\ ( ( O ` ( M ` A ) ) ` A ) = .0. ) )
28	23 27	sylib	|- ( ph -> ( ( M ` A ) e. dom O /\ ( ( O ` ( M ` A ) ) ` A ) = .0. ) )
29	28	simprd	|- ( ph -> ( ( O ` ( M ` A ) ) ` A ) = .0. )