Metamath Proof Explorer

Theorem minplyelirng

Description: If the minimial polynomial F of an element X of a field R has nonnegative degree, then X is integral. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses minplyelirng.b 
|- B = ( Base ` R )
minplyelirng.m 
|- M = ( R minPoly S )
minplyelirng.d 
|- D = ( deg1 ` ( R |`s S ) )
minplyelirng.r 
|- ( ph -> R e. Field )
minplyelirng.s 
|- ( ph -> S e. ( SubDRing ` R ) )
minplyelirng.a 
|- ( ph -> A e. B )
minplyelirng.1 
|- ( ph -> ( D ` ( M ` A ) ) e. NN0 )
Assertion minplyelirng 
|- ( ph -> A e. ( R IntgRing S ) )

Proof

Step Hyp Ref Expression
1 minplyelirng.b 
 |-  B = ( Base ` R )
2 minplyelirng.m 
 |-  M = ( R minPoly S )
3 minplyelirng.d 
 |-  D = ( deg1 ` ( R |`s S ) )
4 minplyelirng.r 
 |-  ( ph -> R e. Field )
5 minplyelirng.s 
 |-  ( ph -> S e. ( SubDRing ` R ) )
6 minplyelirng.a 
 |-  ( ph -> A e. B )
7 minplyelirng.1 
 |-  ( ph -> ( D ` ( M ` A ) ) e. NN0 )
8 fveq2 
 |-  ( m = ( M ` A ) -> ( ( R evalSub1 S ) ` m ) = ( ( R evalSub1 S ) ` ( M ` A ) ) )
9 8 fveq1d 
 |-  ( m = ( M ` A ) -> ( ( ( R evalSub1 S ) ` m ) ` A ) = ( ( ( R evalSub1 S ) ` ( M ` A ) ) ` A ) )
10 9 eqeq1d 
 |-  ( m = ( M ` A ) -> ( ( ( ( R evalSub1 S ) ` m ) ` A ) = ( 0g ` R ) <-> ( ( ( R evalSub1 S ) ` ( M ` A ) ) ` A ) = ( 0g ` R ) ) )
11 eqid 
 |-  ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) )
12 sdrgsubrg 
 |-  ( S e. ( SubDRing ` R ) -> S e. ( SubRing ` R ) )
13 5 12 syl 
 |-  ( ph -> S e. ( SubRing ` R ) )
14 eqid 
 |-  ( R |`s S ) = ( R |`s S )
15 14 subrgring 
 |-  ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
16 13 15 syl 
 |-  ( ph -> ( R |`s S ) e. Ring )
17 eqid 
 |-  ( R evalSub1 S ) = ( R evalSub1 S )
18 eqid 
 |-  ( Poly1 ` ( R |`s S ) ) = ( Poly1 ` ( R |`s S ) )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 eqid 
 |-  { q e. dom ( R evalSub1 S ) | ( ( ( R evalSub1 S ) ` q ) ` A ) = ( 0g ` R ) } = { q e. dom ( R evalSub1 S ) | ( ( ( R evalSub1 S ) ` q ) ` A ) = ( 0g ` R ) }
21 eqid 
 |-  ( RSpan ` ( Poly1 ` ( R |`s S ) ) ) = ( RSpan ` ( Poly1 ` ( R |`s S ) ) )
22 eqid 
 |-  ( idlGen1p ` ( R |`s S ) ) = ( idlGen1p ` ( R |`s S ) )
23 17 18 1 4 5 6 19 20 21 22 2 minplycl 
 |-  ( ph -> ( M ` A ) e. ( Base ` ( Poly1 ` ( R |`s S ) ) ) )
24 eqid 
 |-  ( 0g ` ( Poly1 ` ( R |`s S ) ) ) = ( 0g ` ( Poly1 ` ( R |`s S ) ) )
25 eqid 
 |-  ( Base ` ( Poly1 ` ( R |`s S ) ) ) = ( Base ` ( Poly1 ` ( R |`s S ) ) )
26 3 18 24 25 deg1nn0clb 
 |-  ( ( ( R |`s S ) e. Ring /\ ( M ` A ) e. ( Base ` ( Poly1 ` ( R |`s S ) ) ) ) -> ( ( M ` A ) =/= ( 0g ` ( Poly1 ` ( R |`s S ) ) ) <-> ( D ` ( M ` A ) ) e. NN0 ) )
27 26 biimpar 
 |-  ( ( ( ( R |`s S ) e. Ring /\ ( M ` A ) e. ( Base ` ( Poly1 ` ( R |`s S ) ) ) ) /\ ( D ` ( M ` A ) ) e. NN0 ) -> ( M ` A ) =/= ( 0g ` ( Poly1 ` ( R |`s S ) ) ) )
28 16 23 7 27 syl21anc 
 |-  ( ph -> ( M ` A ) =/= ( 0g ` ( Poly1 ` ( R |`s S ) ) ) )
29 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
30 29 14 18 25 13 11 ressply10g 
 |-  ( ph -> ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` ( R |`s S ) ) ) )
31 28 30 neeqtrrd 
 |-  ( ph -> ( M ` A ) =/= ( 0g ` ( Poly1 ` R ) ) )
32 eqid 
 |-  ( Monic1p ` ( R |`s S ) ) = ( Monic1p ` ( R |`s S ) )
33 1 11 4 5 2 6 31 32 minplynzm1p 
 |-  ( ph -> ( M ` A ) e. ( Monic1p ` ( R |`s S ) ) )
34 17 18 1 4 5 6 19 2 minplyann 
 |-  ( ph -> ( ( ( R evalSub1 S ) ` ( M ` A ) ) ` A ) = ( 0g ` R ) )
35 10 33 34 rspcedvdw 
 |-  ( ph -> E. m e. ( Monic1p ` ( R |`s S ) ) ( ( ( R evalSub1 S ) ` m ) ` A ) = ( 0g ` R ) )
36 4 fldcrngd 
 |-  ( ph -> R e. CRing )
37 17 14 1 19 36 13 elirng 
 |-  ( ph -> ( A e. ( R IntgRing S ) <-> ( A e. B /\ E. m e. ( Monic1p ` ( R |`s S ) ) ( ( ( R evalSub1 S ) ` m ) ` A ) = ( 0g ` R ) ) ) )
38 6 35 37 mpbir2and 
 |-  ( ph -> A e. ( R IntgRing S ) )