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. )