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

Metamath Proof Explorer

Theorem ply1annprmidl

Description: The set Q of polynomials annihilating an element A is a prime ideal. (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. }
Assertion ply1annprmidl 
|- ( ph -> Q e. ( PrmIdeal ` P ) )

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 4 fldcrngd 
 |-  ( ph -> E e. CRing )
10 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
11 5 10 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
12 11 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
13 eqid 
 |-  ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) = ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) )
14 1 2 3 9 12 6 7 8 13 ply1annidllem 
 |-  ( ph -> Q = ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) )
15 eqid 
 |-  ( Base ` P ) = ( Base ` P )
16 1 2 3 15 9 12 6 13 evls1maprhm 
 |-  ( ph -> ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom E ) )
17 fldidom 
 |-  ( E e. Field -> E e. IDomn )
18 7 prmidl0 
 |-  ( ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) <-> E e. IDomn )
19 18 biimpri 
 |-  ( E e. IDomn -> ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) )
20 4 17 19 3syl 
 |-  ( ph -> ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) )
21 20 simprd 
 |-  ( ph -> { .0. } e. ( PrmIdeal ` E ) )
22 eqid 
 |-  ( PrmIdeal ` P ) = ( PrmIdeal ` P )
23 22 rhmpreimaprmidl 
 |-  ( ( ( E e. CRing /\ ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom E ) ) /\ { .0. } e. ( PrmIdeal ` E ) ) -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( PrmIdeal ` P ) )
24 9 16 21 23 syl21anc 
 |-  ( ph -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( PrmIdeal ` P ) )
25 14 24 eqeltrd 
 |-  ( ph -> Q e. ( PrmIdeal ` P ) )