# 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}={\mathrm{Poly}}_{1}\left({R}\right)$
ig1pval.g ${⊢}{G}={idlGen}_{\mathrm{1p}}\left({R}\right)$
ig1pval.z
ig1pval.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
ig1pval.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
ig1pval.m ${⊢}{M}={Monic}_{\mathrm{1p}}\left({R}\right)$
Assertion ig1pval

### Proof

Step Hyp Ref Expression
1 ig1pval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ig1pval.g ${⊢}{G}={idlGen}_{\mathrm{1p}}\left({R}\right)$
3 ig1pval.z
4 ig1pval.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
5 ig1pval.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
6 ig1pval.m ${⊢}{M}={Monic}_{\mathrm{1p}}\left({R}\right)$
7 elex ${⊢}{R}\in {V}\to {R}\in \mathrm{V}$
8 fveq2 ${⊢}{r}={R}\to {\mathrm{Poly}}_{1}\left({r}\right)={\mathrm{Poly}}_{1}\left({R}\right)$
9 8 1 syl6eqr ${⊢}{r}={R}\to {\mathrm{Poly}}_{1}\left({r}\right)={P}$
10 9 fveq2d ${⊢}{r}={R}\to \mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)=\mathrm{LIdeal}\left({P}\right)$
11 10 4 syl6eqr ${⊢}{r}={R}\to \mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)={U}$
12 9 fveq2d ${⊢}{r}={R}\to {0}_{{\mathrm{Poly}}_{1}\left({r}\right)}={0}_{{P}}$
13 12 3 syl6eqr
14 13 sneqd
15 14 eqeq2d
16 fveq2 ${⊢}{r}={R}\to {Monic}_{\mathrm{1p}}\left({r}\right)={Monic}_{\mathrm{1p}}\left({R}\right)$
17 16 6 syl6eqr ${⊢}{r}={R}\to {Monic}_{\mathrm{1p}}\left({r}\right)={M}$
18 17 ineq2d ${⊢}{r}={R}\to {i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)={i}\cap {M}$
19 fveq2 ${⊢}{r}={R}\to {\mathrm{deg}}_{1}\left({r}\right)={\mathrm{deg}}_{1}\left({R}\right)$
20 19 5 syl6eqr ${⊢}{r}={R}\to {\mathrm{deg}}_{1}\left({r}\right)={D}$
21 20 fveq1d ${⊢}{r}={R}\to {\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)={D}\left({g}\right)$
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 ${⊢}{idlGen}_{\mathrm{1p}}=\left({r}\in \mathrm{V}⟼\left({i}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)⟼if\left({i}=\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\},{0}_{{\mathrm{Poly}}_{1}\left({r}\right)},\left(\iota {g}\in \left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)|{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)\right)\right)\right)\right)$
30 28 29 4 mptfvmpt
31 7 30 syl
32 2 31 syl5eq
33 32 fveq1d
34 eqeq1
35 ineq1 ${⊢}{i}={I}\to {i}\cap {M}={I}\cap {M}$
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