Metamath Proof Explorer

Theorem ig1pmindeg

Description: The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025)

Ref Expression
Hypotheses ig1pirred.p 
|- P = ( Poly1 ` R )
ig1pirred.g 
|- G = ( idlGen1p ` R )
ig1pirred.u 
|- U = ( Base ` P )
ig1pirred.r 
|- ( ph -> R e. DivRing )
ig1pirred.1 
|- ( ph -> I e. ( LIdeal ` P ) )
ig1pmindeg.d 
|- D = ( deg1 ` R )
ig1pmindeg.o 
|- .0. = ( 0g ` P )
ig1pmindeg.2 
|- ( ph -> F e. I )
ig1pmindeg.3 
|- ( ph -> F =/= .0. )
Assertion ig1pmindeg 
|- ( ph -> ( D ` ( G ` I ) ) <_ ( D ` F ) )

Proof

Step Hyp Ref Expression
1 ig1pirred.p 
 |-  P = ( Poly1 ` R )
2 ig1pirred.g 
 |-  G = ( idlGen1p ` R )
3 ig1pirred.u 
 |-  U = ( Base ` P )
4 ig1pirred.r 
 |-  ( ph -> R e. DivRing )
5 ig1pirred.1 
 |-  ( ph -> I e. ( LIdeal ` P ) )
6 ig1pmindeg.d 
 |-  D = ( deg1 ` R )
7 ig1pmindeg.o 
 |-  .0. = ( 0g ` P )
8 ig1pmindeg.2 
 |-  ( ph -> F e. I )
9 ig1pmindeg.3 
 |-  ( ph -> F =/= .0. )
10 8 adantr 
 |-  ( ( ph /\ I = { .0. } ) -> F e. I )
11 simpr 
 |-  ( ( ph /\ I = { .0. } ) -> I = { .0. } )
12 10 11 eleqtrd 
 |-  ( ( ph /\ I = { .0. } ) -> F e. { .0. } )
13 elsni 
 |-  ( F e. { .0. } -> F = .0. )
14 12 13 syl 
 |-  ( ( ph /\ I = { .0. } ) -> F = .0. )
15 9 adantr 
 |-  ( ( ph /\ I = { .0. } ) -> F =/= .0. )
16 14 15 pm2.21ddne 
 |-  ( ( ph /\ I = { .0. } ) -> ( D ` ( G ` I ) ) <_ ( D ` F ) )
17 4 adantr 
 |-  ( ( ph /\ I =/= { .0. } ) -> R e. DivRing )
18 5 adantr 
 |-  ( ( ph /\ I =/= { .0. } ) -> I e. ( LIdeal ` P ) )
19 simpr 
 |-  ( ( ph /\ I =/= { .0. } ) -> I =/= { .0. } )
20 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
21 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
22 1 2 7 20 6 21 ig1pval3 
 |-  ( ( R e. DivRing /\ I e. ( LIdeal ` P ) /\ I =/= { .0. } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. ( Monic1p ` R ) /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
23 17 18 19 22 syl3anc 
 |-  ( ( ph /\ I =/= { .0. } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. ( Monic1p ` R ) /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
24 23 simp3d 
 |-  ( ( ph /\ I =/= { .0. } ) -> ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
25 nfv 
 |-  F/ f ( ph /\ I =/= { .0. } )
26 6 1 3 deg1xrf 
 |-  D : U --> RR*
27 26 a1i 
 |-  ( ( ph /\ I =/= { .0. } ) -> D : U --> RR* )
28 27 ffund 
 |-  ( ( ph /\ I =/= { .0. } ) -> Fun D )
29 17 drngringd 
 |-  ( ( ph /\ I =/= { .0. } ) -> R e. Ring )
30 29 adantr 
 |-  ( ( ( ph /\ I =/= { .0. } ) /\ f e. ( I \ { .0. } ) ) -> R e. Ring )
31 3 20 lidlss 
 |-  ( I e. ( LIdeal ` P ) -> I C_ U )
32 18 31 syl 
 |-  ( ( ph /\ I =/= { .0. } ) -> I C_ U )
33 32 ssdifssd 
 |-  ( ( ph /\ I =/= { .0. } ) -> ( I \ { .0. } ) C_ U )
34 33 sselda 
 |-  ( ( ( ph /\ I =/= { .0. } ) /\ f e. ( I \ { .0. } ) ) -> f e. U )
35 eldifsni 
 |-  ( f e. ( I \ { .0. } ) -> f =/= .0. )
36 35 adantl 
 |-  ( ( ( ph /\ I =/= { .0. } ) /\ f e. ( I \ { .0. } ) ) -> f =/= .0. )
37 6 1 7 3 deg1nn0cl 
 |-  ( ( R e. Ring /\ f e. U /\ f =/= .0. ) -> ( D ` f ) e. NN0 )
38 30 34 36 37 syl3anc 
 |-  ( ( ( ph /\ I =/= { .0. } ) /\ f e. ( I \ { .0. } ) ) -> ( D ` f ) e. NN0 )
39 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
40 38 39 eleqtrdi 
 |-  ( ( ( ph /\ I =/= { .0. } ) /\ f e. ( I \ { .0. } ) ) -> ( D ` f ) e. ( ZZ>= ` 0 ) )
41 25 28 40 funimassd 
 |-  ( ( ph /\ I =/= { .0. } ) -> ( D " ( I \ { .0. } ) ) C_ ( ZZ>= ` 0 ) )
42 27 ffnd 
 |-  ( ( ph /\ I =/= { .0. } ) -> D Fn U )
43 8 adantr 
 |-  ( ( ph /\ I =/= { .0. } ) -> F e. I )
44 32 43 sseldd 
 |-  ( ( ph /\ I =/= { .0. } ) -> F e. U )
45 9 adantr 
 |-  ( ( ph /\ I =/= { .0. } ) -> F =/= .0. )
46 nelsn 
 |-  ( F =/= .0. -> -. F e. { .0. } )
47 45 46 syl 
 |-  ( ( ph /\ I =/= { .0. } ) -> -. F e. { .0. } )
48 43 47 eldifd 
 |-  ( ( ph /\ I =/= { .0. } ) -> F e. ( I \ { .0. } ) )
49 42 44 48 fnfvimad 
 |-  ( ( ph /\ I =/= { .0. } ) -> ( D ` F ) e. ( D " ( I \ { .0. } ) ) )
50 infssuzle 
 |-  ( ( ( D " ( I \ { .0. } ) ) C_ ( ZZ>= ` 0 ) /\ ( D ` F ) e. ( D " ( I \ { .0. } ) ) ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <_ ( D ` F ) )
51 41 49 50 syl2anc 
 |-  ( ( ph /\ I =/= { .0. } ) -> inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <_ ( D ` F ) )
52 24 51 eqbrtrd 
 |-  ( ( ph /\ I =/= { .0. } ) -> ( D ` ( G ` I ) ) <_ ( D ` F ) )
53 16 52 pm2.61dane 
 |-  ( ph -> ( D ` ( G ` I ) ) <_ ( D ` F ) )