Metamath Proof Explorer

Theorem ig1pval2

Description: Generator of the zero 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 )
ig1pval2.z 
|- .0. = ( 0g ` P )
Assertion ig1pval2 
|- ( R e. Ring -> ( G ` { .0. } ) = .0. )

Proof

Step Hyp Ref Expression
1 ig1pval.p 
 |-  P = ( Poly1 ` R )
2 ig1pval.g 
 |-  G = ( idlGen1p ` R )
3 ig1pval2.z 
 |-  .0. = ( 0g ` P )
4 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
5 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
6 5 3 lidl0 
 |-  ( P e. Ring -> { .0. } e. ( LIdeal ` P ) )
7 4 6 syl 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` P ) )
8 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
9 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
10 1 2 3 5 8 9 ig1pval 
 |-  ( ( R e. Ring /\ { .0. } e. ( LIdeal ` P ) ) -> ( G ` { .0. } ) = if ( { .0. } = { .0. } , .0. , ( iota_ g e. ( { .0. } i^i ( Monic1p ` R ) ) ( ( deg1 ` R ) ` g ) = inf ( ( ( deg1 ` R ) " ( { .0. } \ { .0. } ) ) , RR , < ) ) ) )
11 7 10 mpdan 
 |-  ( R e. Ring -> ( G ` { .0. } ) = if ( { .0. } = { .0. } , .0. , ( iota_ g e. ( { .0. } i^i ( Monic1p ` R ) ) ( ( deg1 ` R ) ` g ) = inf ( ( ( deg1 ` R ) " ( { .0. } \ { .0. } ) ) , RR , < ) ) ) )
12 eqid 
 |-  { .0. } = { .0. }
13 12 iftruei 
 |-  if ( { .0. } = { .0. } , .0. , ( iota_ g e. ( { .0. } i^i ( Monic1p ` R ) ) ( ( deg1 ` R ) ` g ) = inf ( ( ( deg1 ` R ) " ( { .0. } \ { .0. } ) ) , RR , < ) ) ) = .0.
14 11 13 eqtrdi 
 |-  ( R e. Ring -> ( G ` { .0. } ) = .0. )