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=Poly1R
ig1pval.g G=idlGen1pR
ig1pval.z 0˙=0P
ig1pval.u U=LIdealP
ig1pval.d D=deg1R
ig1pval.m M=Monic1pR
Assertion ig1pval RVIUGI=ifI=0˙0˙ιgIM|Dg=supDI0˙<

Proof

Step Hyp Ref Expression
1 ig1pval.p P=Poly1R
2 ig1pval.g G=idlGen1pR
3 ig1pval.z 0˙=0P
4 ig1pval.u U=LIdealP
5 ig1pval.d D=deg1R
6 ig1pval.m M=Monic1pR
7 elex RVRV
8 fveq2 r=RPoly1r=Poly1R
9 8 1 eqtr4di r=RPoly1r=P
10 9 fveq2d r=RLIdealPoly1r=LIdealP
11 10 4 eqtr4di r=RLIdealPoly1r=U
12 9 fveq2d r=R0Poly1r=0P
13 12 3 eqtr4di r=R0Poly1r=0˙
14 13 sneqd r=R0Poly1r=0˙
15 14 eqeq2d r=Ri=0Poly1ri=0˙
16 fveq2 r=RMonic1pr=Monic1pR
17 16 6 eqtr4di r=RMonic1pr=M
18 17 ineq2d r=RiMonic1pr=iM
19 fveq2 r=Rdeg1r=deg1R
20 19 5 eqtr4di r=Rdeg1r=D
21 20 fveq1d r=Rdeg1rg=Dg
22 14 difeq2d r=Ri0Poly1r=i0˙
23 20 22 imaeq12d r=Rdeg1ri0Poly1r=Di0˙
24 23 infeq1d r=Rsupdeg1ri0Poly1r<=supDi0˙<
25 21 24 eqeq12d r=Rdeg1rg=supdeg1ri0Poly1r<Dg=supDi0˙<
26 18 25 riotaeqbidv r=RιgiMonic1pr|deg1rg=supdeg1ri0Poly1r<=ιgiM|Dg=supDi0˙<
27 15 13 26 ifbieq12d r=Rifi=0Poly1r0Poly1rιgiMonic1pr|deg1rg=supdeg1ri0Poly1r<=ifi=0˙0˙ιgiM|Dg=supDi0˙<
28 11 27 mpteq12dv r=RiLIdealPoly1rifi=0Poly1r0Poly1rιgiMonic1pr|deg1rg=supdeg1ri0Poly1r<=iUifi=0˙0˙ιgiM|Dg=supDi0˙<
29 df-ig1p idlGen1p=rViLIdealPoly1rifi=0Poly1r0Poly1rιgiMonic1pr|deg1rg=supdeg1ri0Poly1r<
30 28 29 4 mptfvmpt RVidlGen1pR=iUifi=0˙0˙ιgiM|Dg=supDi0˙<
31 7 30 syl RVidlGen1pR=iUifi=0˙0˙ιgiM|Dg=supDi0˙<
32 2 31 eqtrid RVG=iUifi=0˙0˙ιgiM|Dg=supDi0˙<
33 32 fveq1d RVGI=iUifi=0˙0˙ιgiM|Dg=supDi0˙<I
34 eqeq1 i=Ii=0˙I=0˙
35 ineq1 i=IiM=IM
36 difeq1 i=Ii0˙=I0˙
37 36 imaeq2d i=IDi0˙=DI0˙
38 37 infeq1d i=IsupDi0˙<=supDI0˙<
39 38 eqeq2d i=IDg=supDi0˙<Dg=supDI0˙<
40 35 39 riotaeqbidv i=IιgiM|Dg=supDi0˙<=ιgIM|Dg=supDI0˙<
41 34 40 ifbieq2d i=Iifi=0˙0˙ιgiM|Dg=supDi0˙<=ifI=0˙0˙ιgIM|Dg=supDI0˙<
42 eqid iUifi=0˙0˙ιgiM|Dg=supDi0˙<=iUifi=0˙0˙ιgiM|Dg=supDi0˙<
43 3 fvexi 0˙V
44 riotaex ιgIM|Dg=supDI0˙<V
45 43 44 ifex ifI=0˙0˙ιgIM|Dg=supDI0˙<V
46 41 42 45 fvmpt IUiUifi=0˙0˙ιgiM|Dg=supDi0˙<I=ifI=0˙0˙ιgIM|Dg=supDI0˙<
47 33 46 sylan9eq RVIUGI=ifI=0˙0˙ιgIM|Dg=supDI0˙<