This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } ) )