This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )