Theorem ply1annig1p

Description: The ideal Q of polynomials annihilating an element A is generated by the ideal's canonical generator. (Contributed by Thierry Arnoux, 9-Feb-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 )
	ply1annig1p.0	|- .0. = ( 0g ` E )
	ply1annig1p.q	|- Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
	ply1annig1p.k	|- K = ( RSpan ` P )
	ply1annig1p.g	|- G = ( idlGen1p ` ( E |`s F ) )
Assertion	ply1annig1p	|- ( ph -> Q = ( K ` { ( G ` Q ) } ) )

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		ply1annig1p.0	|- .0. = ( 0g ` E )
8		ply1annig1p.q	|- Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
9		ply1annig1p.k	|- K = ( RSpan ` P )
10		ply1annig1p.g	|- G = ( idlGen1p ` ( E |`s F ) )
11		issdrg	|- ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
12	5 11	sylib	|- ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
13	12	simp3d	|- ( ph -> ( E |`s F ) e. DivRing )
14	4	fldcrngd	|- ( ph -> E e. CRing )
15	12	simp2d	|- ( ph -> F e. ( SubRing ` E ) )
16	1 2 3 14 15 6 7 8	ply1annidl	|- ( ph -> Q e. ( LIdeal ` P ) )
17		eqid	|- ( LIdeal ` P ) = ( LIdeal ` P )
18	2 10 17 9	ig1prsp	|- ( ( ( E |`s F ) e. DivRing /\ Q e. ( LIdeal ` P ) ) -> Q = ( K ` { ( G ` Q ) } ) )
19	13 16 18	syl2anc	|- ( ph -> Q = ( K ` { ( G ` Q ) } ) )