Metamath Proof Explorer

Theorem irngnminplynz

Description: Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses irngnminplynz.z 
|- Z = ( 0g ` ( Poly1 ` E ) )
irngnminplynz.e 
|- ( ph -> E e. Field )
irngnminplynz.f 
|- ( ph -> F e. ( SubDRing ` E ) )
irngnminplynz.m 
|- M = ( E minPoly F )
irngnminplynz.a 
|- ( ph -> A e. ( E IntgRing F ) )
Assertion irngnminplynz 
|- ( ph -> ( M ` A ) =/= Z )

Proof

Step Hyp Ref Expression
1 irngnminplynz.z 
 |-  Z = ( 0g ` ( Poly1 ` E ) )
2 irngnminplynz.e 
 |-  ( ph -> E e. Field )
3 irngnminplynz.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
4 irngnminplynz.m 
 |-  M = ( E minPoly F )
5 irngnminplynz.a 
 |-  ( ph -> A e. ( E IntgRing F ) )
6 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
7 3 6 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
8 eqid 
 |-  ( E |`s F ) = ( E |`s F )
9 8 subrgring 
 |-  ( F e. ( SubRing ` E ) -> ( E |`s F ) e. Ring )
10 7 9 syl 
 |-  ( ph -> ( E |`s F ) e. Ring )
11 eqid 
 |-  ( Poly1 ` ( E |`s F ) ) = ( Poly1 ` ( E |`s F ) )
12 11 ply1ring 
 |-  ( ( E |`s F ) e. Ring -> ( Poly1 ` ( E |`s F ) ) e. Ring )
13 10 12 syl 
 |-  ( ph -> ( Poly1 ` ( E |`s F ) ) e. Ring )
14 eqid 
 |-  ( E evalSub1 F ) = ( E evalSub1 F )
15 eqid 
 |-  ( Base ` E ) = ( Base ` E )
16 2 fldcrngd 
 |-  ( ph -> E e. CRing )
17 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
18 14 8 15 17 16 7 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
19 18 5 sseldd 
 |-  ( ph -> A e. ( Base ` E ) )
20 eqid 
 |-  { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } = { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) }
21 14 11 15 16 7 19 17 20 ply1annidl 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) )
22 eqid 
 |-  ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( Poly1 ` ( E |`s F ) ) )
23 eqid 
 |-  ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) = ( LIdeal ` ( Poly1 ` ( E |`s F ) ) )
24 22 23 lidlss 
 |-  ( { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } C_ ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
25 21 24 syl 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } C_ ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
26 8 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
27 3 26 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
28 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
29 11 28 23 ig1pcl 
 |-  ( ( ( E |`s F ) e. DivRing /\ { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) ) -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } )
30 27 21 29 syl2anc 
 |-  ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } )
31 25 30 sseldd 
 |-  ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
32 eqid 
 |-  ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) = ( RSpan ` ( Poly1 ` ( E |`s F ) ) )
33 14 11 15 2 3 19 17 20 32 28 ply1annig1p 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } = ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) )
34 fveq2 
 |-  ( q = p -> ( ( E evalSub1 F ) ` q ) = ( ( E evalSub1 F ) ` p ) )
35 34 fveq1d 
 |-  ( q = p -> ( ( ( E evalSub1 F ) ` q ) ` A ) = ( ( ( E evalSub1 F ) ` p ) ` A ) )
36 35 eqeq1d 
 |-  ( q = p -> ( ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) <-> ( ( ( E evalSub1 F ) ` p ) ` A ) = ( 0g ` E ) ) )
37 simplr 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> p e. ( dom ( E evalSub1 F ) \ { Z } ) )
38 37 eldifad 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> p e. dom ( E evalSub1 F ) )
39 16 ad2antrr 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> E e. CRing )
40 7 ad2antrr 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> F e. ( SubRing ` E ) )
41 14 11 22 16 7 evls1dm 
 |-  ( ph -> dom ( E evalSub1 F ) = ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> dom ( E evalSub1 F ) = ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
43 38 42 eleqtrd 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> p e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
44 14 11 22 39 40 15 43 evls1fvf 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> ( ( E evalSub1 F ) ` p ) : ( Base ` E ) --> ( Base ` E ) )
45 44 ffnd 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> ( ( E evalSub1 F ) ` p ) Fn ( Base ` E ) )
46 elpreima 
 |-  ( ( ( E evalSub1 F ) ` p ) Fn ( Base ` E ) -> ( A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) <-> ( A e. ( Base ` E ) /\ ( ( ( E evalSub1 F ) ` p ) ` A ) e. { ( 0g ` E ) } ) ) )
47 46 simplbda 
 |-  ( ( ( ( E evalSub1 F ) ` p ) Fn ( Base ` E ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> ( ( ( E evalSub1 F ) ` p ) ` A ) e. { ( 0g ` E ) } )
48 45 47 sylancom 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> ( ( ( E evalSub1 F ) ` p ) ` A ) e. { ( 0g ` E ) } )
49 elsni 
 |-  ( ( ( ( E evalSub1 F ) ` p ) ` A ) e. { ( 0g ` E ) } -> ( ( ( E evalSub1 F ) ` p ) ` A ) = ( 0g ` E ) )
50 48 49 syl 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> ( ( ( E evalSub1 F ) ` p ) ` A ) = ( 0g ` E ) )
51 36 38 50 elrabd 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> p e. { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } )
52 eldifsni 
 |-  ( p e. ( dom ( E evalSub1 F ) \ { Z } ) -> p =/= Z )
53 37 52 syl 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> p =/= Z )
54 eqid 
 |-  ( Poly1 ` E ) = ( Poly1 ` E )
55 54 8 11 22 7 1 ressply10g 
 |-  ( ph -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
56 55 ad2antrr 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
57 53 56 neeqtrd 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> p =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
58 nelsn 
 |-  ( p =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) -> -. p e. { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
59 57 58 syl 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> -. p e. { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
60 nelne1 
 |-  ( ( p e. { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } /\ -. p e. { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
61 51 59 60 syl2anc 
 |-  ( ( ( ph /\ p e. ( dom ( E evalSub1 F ) \ { Z } ) ) /\ A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) ) -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
62 14 1 17 2 3 irngnzply1 
 |-  ( ph -> ( E IntgRing F ) = U_ p e. ( dom ( E evalSub1 F ) \ { Z } ) ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) )
63 5 62 eleqtrd 
 |-  ( ph -> A e. U_ p e. ( dom ( E evalSub1 F ) \ { Z } ) ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) )
64 eliun 
 |-  ( A e. U_ p e. ( dom ( E evalSub1 F ) \ { Z } ) ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) <-> E. p e. ( dom ( E evalSub1 F ) \ { Z } ) A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) )
65 63 64 sylib 
 |-  ( ph -> E. p e. ( dom ( E evalSub1 F ) \ { Z } ) A e. ( `' ( ( E evalSub1 F ) ` p ) " { ( 0g ` E ) } ) )
66 61 65 r19.29a 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
67 33 66 eqnetrrd 
 |-  ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
68 eqid 
 |-  ( 0g ` ( Poly1 ` ( E |`s F ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) )
69 22 68 32 pidlnzb 
 |-  ( ( ( Poly1 ` ( E |`s F ) ) e. Ring /\ ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) ) -> ( ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) <-> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) )
70 69 biimpar 
 |-  ( ( ( ( Poly1 ` ( E |`s F ) ) e. Ring /\ ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) ) /\ ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
71 13 31 67 70 syl21anc 
 |-  ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
72 14 11 15 2 3 19 17 20 32 28 4 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) )
73 71 72 55 3netr4d 
 |-  ( ph -> ( M ` A ) =/= Z )