Theorem ig1pcl

Description: The monic generator of an ideal is always in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ig1pval.g	⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
	ig1pcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
Assertion	ig1pcl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ig1pval.g	⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
3		ig1pcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
4		fveq2	⊢ ( 𝐼 = { ( 0g ‘ 𝑃 ) } → ( 𝐺 ‘ 𝐼 ) = ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) )
5		id	⊢ ( 𝐼 = { ( 0g ‘ 𝑃 ) } → 𝐼 = { ( 0g ‘ 𝑃 ) } )
6	4 5	eleq12d	⊢ ( 𝐼 = { ( 0g ‘ 𝑃 ) } → ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ↔ ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) ∈ { ( 0g ‘ 𝑃 ) } ) )
7		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
8		eqid	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
9		eqid	⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
10	1 2 7 3 8 9	ig1pval3	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { ( 0g ‘ 𝑃 ) } ) → ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Monic1p ‘ 𝑅 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝐼 ) ) = inf ( ( ( deg1 ‘ 𝑅 ) “ ( 𝐼 ∖ { ( 0g ‘ 𝑃 ) } ) ) , ℝ , < ) ) )
11	10	simp1d	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { ( 0g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
12	11	3expa	⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) ∧ 𝐼 ≠ { ( 0g ‘ 𝑃 ) } ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
13		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
14	1 2 7	ig1pval2	⊢ ( 𝑅 ∈ Ring → ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) = ( 0g ‘ 𝑃 ) )
15	13 14	syl	⊢ ( 𝑅 ∈ DivRing → ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) = ( 0g ‘ 𝑃 ) )
16		fvex	⊢ ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) ∈ V
17	16	elsn	⊢ ( ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) ∈ { ( 0g ‘ 𝑃 ) } ↔ ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) = ( 0g ‘ 𝑃 ) )
18	15 17	sylibr	⊢ ( 𝑅 ∈ DivRing → ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) ∈ { ( 0g ‘ 𝑃 ) } )
19	18	adantr	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ { ( 0g ‘ 𝑃 ) } ) ∈ { ( 0g ‘ 𝑃 ) } )
20	6 12 19	pm2.61ne	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )