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