Metamath Proof Explorer

Theorem minplym1p

Description: A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-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 ) )
minplym1p.1 
|- U = ( Monic1p ` ( E |`s F ) )
Assertion minplym1p 
|- ( ph -> ( M ` A ) e. U )

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 minplym1p.1 
 |-  U = ( Monic1p ` ( E |`s F ) )
7 eqid 
 |-  ( E evalSub1 F ) = ( E evalSub1 F )
8 eqid 
 |-  ( Poly1 ` ( E |`s F ) ) = ( Poly1 ` ( E |`s F ) )
9 eqid 
 |-  ( Base ` E ) = ( Base ` E )
10 eqid 
 |-  ( E |`s F ) = ( E |`s F )
11 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
12 2 fldcrngd 
 |-  ( ph -> E e. CRing )
13 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
14 3 13 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
15 7 10 9 11 12 14 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
16 15 5 sseldd 
 |-  ( ph -> A e. ( Base ` E ) )
17 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 ) }
18 eqid 
 |-  ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) = ( RSpan ` ( Poly1 ` ( E |`s F ) ) )
19 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
20 7 8 9 2 3 16 11 17 18 19 4 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) )
21 10 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
22 3 21 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
23 7 8 9 12 14 16 11 17 ply1annidl 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) )
24 20 sneqd 
 |-  ( ph -> { ( M ` A ) } = { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } )
25 24 fveq2d 
 |-  ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) = ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) )
26 7 8 9 2 3 16 11 17 18 19 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 ) } ) } ) )
27 25 26 eqtr4d 
 |-  ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) = { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } )
28 22 drngringd 
 |-  ( ph -> ( E |`s F ) e. Ring )
29 8 ply1ring 
 |-  ( ( E |`s F ) e. Ring -> ( Poly1 ` ( E |`s F ) ) e. Ring )
30 28 29 syl 
 |-  ( ph -> ( Poly1 ` ( E |`s F ) ) e. Ring )
31 7 8 9 2 3 16 11 17 18 19 4 minplycl 
 |-  ( ph -> ( M ` A ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
32 1 2 3 4 5 irngnminplynz 
 |-  ( ph -> ( M ` A ) =/= Z )
33 eqid 
 |-  ( Poly1 ` E ) = ( Poly1 ` E )
34 eqid 
 |-  ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( Poly1 ` ( E |`s F ) ) )
35 33 10 8 34 14 1 ressply10g 
 |-  ( ph -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
36 32 35 neeqtrd 
 |-  ( ph -> ( M ` A ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
37 eqid 
 |-  ( 0g ` ( Poly1 ` ( E |`s F ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) )
38 34 37 18 pidlnz 
 |-  ( ( ( Poly1 ` ( E |`s F ) ) e. Ring /\ ( M ` A ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) /\ ( M ` A ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
39 30 31 36 38 syl3anc 
 |-  ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
40 27 39 eqnetrrd 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
41 eqid 
 |-  ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) = ( LIdeal ` ( Poly1 ` ( E |`s F ) ) )
42 eqid 
 |-  ( deg1 ` ( E |`s F ) ) = ( deg1 ` ( E |`s F ) )
43 8 19 37 41 42 6 ig1pval3 
 |-  ( ( ( E |`s F ) e. DivRing /\ { 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 ) } =/= { ( 0g ` ( 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 ) } /\ ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. U /\ ( ( deg1 ` ( E |`s F ) ) ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) ) = inf ( ( ( deg1 ` ( E |`s F ) ) " ( { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } \ { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) ) , RR , < ) ) )
44 22 23 40 43 syl3anc 
 |-  ( 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 ) } /\ ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. U /\ ( ( deg1 ` ( E |`s F ) ) ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) ) = inf ( ( ( deg1 ` ( E |`s F ) ) " ( { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } \ { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) ) , RR , < ) ) )
45 44 simp2d 
 |-  ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. U )
46 20 45 eqeltrd 
 |-  ( ph -> ( M ` A ) e. U )