# Metamath Proof Explorer

## Theorem ig1pval3

Description: Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1pval.p
`|- P = ( Poly1 ` R )`
ig1pval.g
`|- G = ( idlGen1p ` R )`
ig1pval3.z
`|- .0. = ( 0g ` P )`
ig1pval3.u
`|- U = ( LIdeal ` P )`
ig1pval3.d
`|- D = ( deg1 ` R )`
ig1pval3.m
`|- M = ( Monic1p ` R )`
Assertion ig1pval3
`|- ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. M /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`

### Proof

Step Hyp Ref Expression
1 ig1pval.p
` |-  P = ( Poly1 ` R )`
2 ig1pval.g
` |-  G = ( idlGen1p ` R )`
3 ig1pval3.z
` |-  .0. = ( 0g ` P )`
4 ig1pval3.u
` |-  U = ( LIdeal ` P )`
5 ig1pval3.d
` |-  D = ( deg1 ` R )`
6 ig1pval3.m
` |-  M = ( Monic1p ` R )`
7 1 2 3 4 5 6 ig1pval
` |-  ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) )`
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( G ` I ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) )`
9 simp3
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> I =/= { .0. } )`
10 9 neneqd
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> -. I = { .0. } )`
11 10 iffalsed
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) = ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`
12 8 11 eqtrd
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( G ` I ) = ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`
13 1 4 3 6 5 ig1peu
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> E! g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )`
14 riotacl2
` |-  ( E! g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) -> ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) e. { g e. ( I i^i M ) | ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) } )`
15 13 14 syl
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) e. { g e. ( I i^i M ) | ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) } )`
16 12 15 eqeltrd
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( G ` I ) e. { g e. ( I i^i M ) | ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) } )`
17 elin
` |-  ( ( G ` I ) e. ( I i^i M ) <-> ( ( G ` I ) e. I /\ ( G ` I ) e. M ) )`
18 17 anbi1i
` |-  ( ( ( G ` I ) e. ( I i^i M ) /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) <-> ( ( ( G ` I ) e. I /\ ( G ` I ) e. M ) /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`
19 fveqeq2
` |-  ( g = ( G ` I ) -> ( ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) <-> ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`
20 19 elrab
` |-  ( ( G ` I ) e. { g e. ( I i^i M ) | ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) } <-> ( ( G ` I ) e. ( I i^i M ) /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`
21 df-3an
` |-  ( ( ( G ` I ) e. I /\ ( G ` I ) e. M /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) <-> ( ( ( G ` I ) e. I /\ ( G ` I ) e. M ) /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`
22 18 20 21 3bitr4i
` |-  ( ( G ` I ) e. { g e. ( I i^i M ) | ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) } <-> ( ( G ` I ) e. I /\ ( G ` I ) e. M /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`
23 16 22 sylib
` |-  ( ( R e. DivRing /\ I e. U /\ I =/= { .0. } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. M /\ ( D ` ( G ` I ) ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )`