# 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 𝑃 = ( Poly1𝑅 )
ig1pval.g 𝐺 = ( idlGen1p𝑅 )
ig1pval3.z 0 = ( 0g𝑃 )
ig1pval3.u 𝑈 = ( LIdeal ‘ 𝑃 )
ig1pval3.d 𝐷 = ( deg1𝑅 )
ig1pval3.m 𝑀 = ( Monic1p𝑅 )
Assertion ig1pval3 ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ 𝑀 ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )

### Proof

Step Hyp Ref Expression
1 ig1pval.p 𝑃 = ( Poly1𝑅 )
2 ig1pval.g 𝐺 = ( idlGen1p𝑅 )
3 ig1pval3.z 0 = ( 0g𝑃 )
4 ig1pval3.u 𝑈 = ( LIdeal ‘ 𝑃 )
5 ig1pval3.d 𝐷 = ( deg1𝑅 )
6 ig1pval3.m 𝑀 = ( Monic1p𝑅 )
7 1 2 3 4 5 6 ig1pval ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈 ) → ( 𝐺𝐼 ) = if ( 𝐼 = { 0 } , 0 , ( 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) )
8 7 3adant3 ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ( 𝐺𝐼 ) = if ( 𝐼 = { 0 } , 0 , ( 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) )
9 simp3 ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → 𝐼 ≠ { 0 } )
10 9 neneqd ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ¬ 𝐼 = { 0 } )
11 10 iffalsed ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → if ( 𝐼 = { 0 } , 0 , ( 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) = ( 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
12 8 11 eqtrd ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ( 𝐺𝐼 ) = ( 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
13 1 4 3 6 5 ig1peu ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ∃! 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
14 riotacl2 ( ∃! 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) → ( 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ∈ { 𝑔 ∈ ( 𝐼𝑀 ) ∣ ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) } )
15 13 14 syl ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ( 𝑔 ∈ ( 𝐼𝑀 ) ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ∈ { 𝑔 ∈ ( 𝐼𝑀 ) ∣ ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) } )
16 12 15 eqeltrd ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ( 𝐺𝐼 ) ∈ { 𝑔 ∈ ( 𝐼𝑀 ) ∣ ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) } )
17 elin ( ( 𝐺𝐼 ) ∈ ( 𝐼𝑀 ) ↔ ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ 𝑀 ) )
18 17 anbi1i ( ( ( 𝐺𝐼 ) ∈ ( 𝐼𝑀 ) ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ↔ ( ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ 𝑀 ) ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
19 fveqeq2 ( 𝑔 = ( 𝐺𝐼 ) → ( ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ↔ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
20 19 elrab ( ( 𝐺𝐼 ) ∈ { 𝑔 ∈ ( 𝐼𝑀 ) ∣ ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) } ↔ ( ( 𝐺𝐼 ) ∈ ( 𝐼𝑀 ) ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
21 df-3an ( ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ 𝑀 ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ↔ ( ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ 𝑀 ) ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
22 18 20 21 3bitr4i ( ( 𝐺𝐼 ) ∈ { 𝑔 ∈ ( 𝐼𝑀 ) ∣ ( 𝐷𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) } ↔ ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ 𝑀 ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
23 16 22 sylib ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 } ) → ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ 𝑀 ∧ ( 𝐷 ‘ ( 𝐺𝐼 ) ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )