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

Metamath Proof Explorer

Theorem minplynzm1p

Description: If a minimal polynomial is nonzero, then it is monic. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses minplynzm1p.b 
|- B = ( Base ` E )
minplynzm1p.z 
|- Z = ( 0g ` ( Poly1 ` E ) )
minplynzm1p.e 
|- ( ph -> E e. Field )
minplynzm1p.f 
|- ( ph -> F e. ( SubDRing ` E ) )
minplynzm1p.m 
|- M = ( E minPoly F )
minplynzm1p.a 
|- ( ph -> A e. B )
minplynzm1p.1 
|- ( ph -> ( M ` A ) =/= Z )
minplynzm1p.u 
|- U = ( Monic1p ` ( E |`s F ) )
Assertion minplynzm1p 
|- ( ph -> ( M ` A ) e. U )

Proof

Step Hyp Ref Expression
1 minplynzm1p.b 
 |-  B = ( Base ` E )
2 minplynzm1p.z 
 |-  Z = ( 0g ` ( Poly1 ` E ) )
3 minplynzm1p.e 
 |-  ( ph -> E e. Field )
4 minplynzm1p.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
5 minplynzm1p.m 
 |-  M = ( E minPoly F )
6 minplynzm1p.a 
 |-  ( ph -> A e. B )
7 minplynzm1p.1 
 |-  ( ph -> ( M ` A ) =/= Z )
8 minplynzm1p.u 
 |-  U = ( Monic1p ` ( E |`s F ) )
9 eqid 
 |-  ( E evalSub1 F ) = ( E evalSub1 F )
10 eqid 
 |-  ( Poly1 ` ( E |`s F ) ) = ( Poly1 ` ( E |`s F ) )
11 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
12 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 ) }
13 eqid 
 |-  ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) = ( RSpan ` ( Poly1 ` ( E |`s F ) ) )
14 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
15 9 10 1 3 4 6 11 12 13 14 5 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) )
16 eqid 
 |-  ( E |`s F ) = ( E |`s F )
17 16 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
18 4 17 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
19 3 fldcrngd 
 |-  ( ph -> E e. CRing )
20 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
21 4 20 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
22 9 10 1 19 21 6 11 12 ply1annidl 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) )
23 15 sneqd 
 |-  ( ph -> { ( M ` A ) } = { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } )
24 23 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 ) } ) } ) )
25 9 10 1 3 4 6 11 12 13 14 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 ) } ) } ) )
26 24 25 eqtr4d 
 |-  ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) = { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } )
27 18 drngringd 
 |-  ( ph -> ( E |`s F ) e. Ring )
28 10 ply1ring 
 |-  ( ( E |`s F ) e. Ring -> ( Poly1 ` ( E |`s F ) ) e. Ring )
29 27 28 syl 
 |-  ( ph -> ( Poly1 ` ( E |`s F ) ) e. Ring )
30 9 10 1 3 4 6 11 12 13 14 5 minplycl 
 |-  ( ph -> ( M ` A ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
31 eqid 
 |-  ( Poly1 ` E ) = ( Poly1 ` E )
32 eqid 
 |-  ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( Poly1 ` ( E |`s F ) ) )
33 31 16 10 32 21 2 ressply10g 
 |-  ( ph -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
34 7 33 neeqtrd 
 |-  ( ph -> ( M ` A ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
35 eqid 
 |-  ( 0g ` ( Poly1 ` ( E |`s F ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) )
36 32 35 13 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 ) ) ) } )
37 29 30 34 36 syl3anc 
 |-  ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
38 26 37 eqnetrrd 
 |-  ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } )
39 eqid 
 |-  ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) = ( LIdeal ` ( Poly1 ` ( E |`s F ) ) )
40 eqid 
 |-  ( deg1 ` ( E |`s F ) ) = ( deg1 ` ( E |`s F ) )
41 10 14 35 39 40 8 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 , < ) ) )
42 18 22 38 41 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 , < ) ) )
43 42 simp2d 
 |-  ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. U )
44 15 43 eqeltrd 
 |-  ( ph -> ( M ` A ) e. U )