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 | |
|
ig1pval.g | |
||
ig1pval.z | |
||
ig1pval.u | |
||
ig1pval.d | |
||
ig1pval.m | |
||
Assertion | ig1pval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ig1pval.p | |
|
2 | ig1pval.g | |
|
3 | ig1pval.z | |
|
4 | ig1pval.u | |
|
5 | ig1pval.d | |
|
6 | ig1pval.m | |
|
7 | elex | |
|
8 | fveq2 | |
|
9 | 8 1 | eqtr4di | |
10 | 9 | fveq2d | |
11 | 10 4 | eqtr4di | |
12 | 9 | fveq2d | |
13 | 12 3 | eqtr4di | |
14 | 13 | sneqd | |
15 | 14 | eqeq2d | |
16 | fveq2 | |
|
17 | 16 6 | eqtr4di | |
18 | 17 | ineq2d | |
19 | fveq2 | |
|
20 | 19 5 | eqtr4di | |
21 | 20 | fveq1d | |
22 | 14 | difeq2d | |
23 | 20 22 | imaeq12d | |
24 | 23 | infeq1d | |
25 | 21 24 | eqeq12d | |
26 | 18 25 | riotaeqbidv | |
27 | 15 13 26 | ifbieq12d | |
28 | 11 27 | mpteq12dv | |
29 | df-ig1p | |
|
30 | 28 29 4 | mptfvmpt | |
31 | 7 30 | syl | |
32 | 2 31 | eqtrid | |
33 | 32 | fveq1d | |
34 | eqeq1 | |
|
35 | ineq1 | |
|
36 | difeq1 | |
|
37 | 36 | imaeq2d | |
38 | 37 | infeq1d | |
39 | 38 | eqeq2d | |
40 | 35 39 | riotaeqbidv | |
41 | 34 40 | ifbieq2d | |
42 | eqid | |
|
43 | 3 | fvexi | |
44 | riotaex | |
|
45 | 43 44 | ifex | |
46 | 41 42 45 | fvmpt | |
47 | 33 46 | sylan9eq | |