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 
|- P = ( Poly1 ` R )
ig1pval.g 
|- G = ( idlGen1p ` R )
ig1pcl.u 
|- U = ( LIdeal ` P )
Assertion ig1pcl 
|- ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) e. I )

Proof

Step Hyp Ref Expression
1 ig1pval.p 
 |-  P = ( Poly1 ` R )
2 ig1pval.g 
 |-  G = ( idlGen1p ` R )
3 ig1pcl.u 
 |-  U = ( LIdeal ` P )
4 fveq2 
 |-  ( I = { ( 0g ` P ) } -> ( G ` I ) = ( G ` { ( 0g ` P ) } ) )
5 id 
 |-  ( I = { ( 0g ` P ) } -> I = { ( 0g ` P ) } )
6 4 5 eleq12d 
 |-  ( I = { ( 0g ` P ) } -> ( ( G ` I ) e. I <-> ( G ` { ( 0g ` P ) } ) e. { ( 0g ` P ) } ) )
7 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
8 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
9 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
10 1 2 7 3 8 9 ig1pval3 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { ( 0g ` P ) } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. ( Monic1p ` R ) /\ ( ( deg1 ` R ) ` ( G ` I ) ) = inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) ) )
11 10 simp1d 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { ( 0g ` P ) } ) -> ( G ` I ) e. I )
12 11 3expa 
 |-  ( ( ( R e. DivRing /\ I e. U ) /\ I =/= { ( 0g ` P ) } ) -> ( G ` I ) e. I )
13 drngring 
 |-  ( R e. DivRing -> R e. Ring )
14 1 2 7 ig1pval2 
 |-  ( R e. Ring -> ( G ` { ( 0g ` P ) } ) = ( 0g ` P ) )
15 13 14 syl 
 |-  ( R e. DivRing -> ( G ` { ( 0g ` P ) } ) = ( 0g ` P ) )
16 fvex 
 |-  ( G ` { ( 0g ` P ) } ) e. _V
17 16 elsn 
 |-  ( ( G ` { ( 0g ` P ) } ) e. { ( 0g ` P ) } <-> ( G ` { ( 0g ` P ) } ) = ( 0g ` P ) )
18 15 17 sylibr 
 |-  ( R e. DivRing -> ( G ` { ( 0g ` P ) } ) e. { ( 0g ` P ) } )
19 18 adantr 
 |-  ( ( R e. DivRing /\ I e. U ) -> ( G ` { ( 0g ` P ) } ) e. { ( 0g ` P ) } )
20 6 12 19 pm2.61ne 
 |-  ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) e. I )