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 } ) ) , ℝ , < ) ) )