Metamath Proof Explorer

Theorem ig1pval

Description: Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1pval.p 
|- P = ( Poly1 ` R )
ig1pval.g 
|- G = ( idlGen1p ` R )
ig1pval.z 
|- .0. = ( 0g ` P )
ig1pval.u 
|- U = ( LIdeal ` P )
ig1pval.d 
|- D = ( deg1 ` R )
ig1pval.m 
|- M = ( Monic1p ` R )
Assertion ig1pval 
|- ( ( R e. V /\ I e. U ) -> ( G ` I ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) )

Proof

Step Hyp Ref Expression
1 ig1pval.p 
 |-  P = ( Poly1 ` R )
2 ig1pval.g 
 |-  G = ( idlGen1p ` R )
3 ig1pval.z 
 |-  .0. = ( 0g ` P )
4 ig1pval.u 
 |-  U = ( LIdeal ` P )
5 ig1pval.d 
 |-  D = ( deg1 ` R )
6 ig1pval.m 
 |-  M = ( Monic1p ` R )
7 elex 
 |-  ( R e. V -> R e. _V )
8 fveq2 
 |-  ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
9 8 1 eqtr4di 
 |-  ( r = R -> ( Poly1 ` r ) = P )
10 9 fveq2d 
 |-  ( r = R -> ( LIdeal ` ( Poly1 ` r ) ) = ( LIdeal ` P ) )
11 10 4 eqtr4di 
 |-  ( r = R -> ( LIdeal ` ( Poly1 ` r ) ) = U )
12 9 fveq2d 
 |-  ( r = R -> ( 0g ` ( Poly1 ` r ) ) = ( 0g ` P ) )
13 12 3 eqtr4di 
 |-  ( r = R -> ( 0g ` ( Poly1 ` r ) ) = .0. )
14 13 sneqd 
 |-  ( r = R -> { ( 0g ` ( Poly1 ` r ) ) } = { .0. } )
15 14 eqeq2d 
 |-  ( r = R -> ( i = { ( 0g ` ( Poly1 ` r ) ) } <-> i = { .0. } ) )
16 fveq2 
 |-  ( r = R -> ( Monic1p ` r ) = ( Monic1p ` R ) )
17 16 6 eqtr4di 
 |-  ( r = R -> ( Monic1p ` r ) = M )
18 17 ineq2d 
 |-  ( r = R -> ( i i^i ( Monic1p ` r ) ) = ( i i^i M ) )
19 fveq2 
 |-  ( r = R -> ( deg1 ` r ) = ( deg1 ` R ) )
20 19 5 eqtr4di 
 |-  ( r = R -> ( deg1 ` r ) = D )
21 20 fveq1d 
 |-  ( r = R -> ( ( deg1 ` r ) ` g ) = ( D ` g ) )
22 14 difeq2d 
 |-  ( r = R -> ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) = ( i \ { .0. } ) )
23 20 22 imaeq12d 
 |-  ( r = R -> ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) = ( D " ( i \ { .0. } ) ) )
24 23 infeq1d 
 |-  ( r = R -> inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) )
25 21 24 eqeq12d 
 |-  ( r = R -> ( ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) <-> ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) )
26 18 25 riotaeqbidv 
 |-  ( r = R -> ( iota_ g e. ( i i^i ( Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) = ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) )
27 15 13 26 ifbieq12d 
 |-  ( r = R -> if ( i = { ( 0g ` ( Poly1 ` r ) ) } , ( 0g ` ( Poly1 ` r ) ) , ( iota_ g e. ( i i^i ( Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) ) = if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) )
28 11 27 mpteq12dv 
 |-  ( r = R -> ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> if ( i = { ( 0g ` ( Poly1 ` r ) ) } , ( 0g ` ( Poly1 ` r ) ) , ( iota_ g e. ( i i^i ( Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) ) ) = ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) ) )
29 df-ig1p 
 |-  idlGen1p = ( r e. _V |-> ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> if ( i = { ( 0g ` ( Poly1 ` r ) ) } , ( 0g ` ( Poly1 ` r ) ) , ( iota_ g e. ( i i^i ( Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) ) ) )
30 28 29 4 mptfvmpt 
 |-  ( R e. _V -> ( idlGen1p ` R ) = ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) ) )
31 7 30 syl 
 |-  ( R e. V -> ( idlGen1p ` R ) = ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) ) )
32 2 31 syl5eq 
 |-  ( R e. V -> G = ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) ) )
33 32 fveq1d 
 |-  ( R e. V -> ( G ` I ) = ( ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) ) ` I ) )
34 eqeq1 
 |-  ( i = I -> ( i = { .0. } <-> I = { .0. } ) )
35 ineq1 
 |-  ( i = I -> ( i i^i M ) = ( I i^i M ) )
36 difeq1 
 |-  ( i = I -> ( i \ { .0. } ) = ( I \ { .0. } ) )
37 36 imaeq2d 
 |-  ( i = I -> ( D " ( i \ { .0. } ) ) = ( D " ( I \ { .0. } ) ) )
38 37 infeq1d 
 |-  ( i = I -> inf ( ( D " ( i \ { .0. } ) ) , RR , < ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) )
39 38 eqeq2d 
 |-  ( i = I -> ( ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) <-> ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
40 35 39 riotaeqbidv 
 |-  ( i = I -> ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) = ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) )
41 34 40 ifbieq2d 
 |-  ( i = I -> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) )
42 eqid 
 |-  ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) ) = ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) )
43 3 fvexi 
 |-  .0. e. _V
44 riotaex 
 |-  ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) e. _V
45 43 44 ifex 
 |-  if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) e. _V
46 41 42 45 fvmpt 
 |-  ( I e. U -> ( ( i e. U |-> if ( i = { .0. } , .0. , ( iota_ g e. ( i i^i M ) ( D ` g ) = inf ( ( D " ( i \ { .0. } ) ) , RR , < ) ) ) ) ` I ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) )
47 33 46 sylan9eq 
 |-  ( ( R e. V /\ I e. U ) -> ( G ` I ) = if ( I = { .0. } , .0. , ( iota_ g e. ( I i^i M ) ( D ` g ) = inf ( ( D " ( I \ { .0. } ) ) , RR , < ) ) ) )