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 = Poly 1 R
ig1pval.g G = idlGen 1p R
ig1pval.z 0 ˙ = 0 P
ig1pval.u U = LIdeal P
ig1pval.d D = deg 1 R
ig1pval.m M = Monic 1p R
Assertion ig1pval R V I U G I = if I = 0 ˙ 0 ˙ ι g I M | D g = sup D I 0 ˙ <

Proof

Step Hyp Ref Expression
1 ig1pval.p P = Poly 1 R
2 ig1pval.g G = idlGen 1p R
3 ig1pval.z 0 ˙ = 0 P
4 ig1pval.u U = LIdeal P
5 ig1pval.d D = deg 1 R
6 ig1pval.m M = Monic 1p R
7 elex R V R V
8 fveq2 r = R Poly 1 r = Poly 1 R
9 8 1 eqtr4di r = R Poly 1 r = P
10 9 fveq2d r = R LIdeal Poly 1 r = LIdeal P
11 10 4 eqtr4di r = R LIdeal Poly 1 r = U
12 9 fveq2d r = R 0 Poly 1 r = 0 P
13 12 3 eqtr4di r = R 0 Poly 1 r = 0 ˙
14 13 sneqd r = R 0 Poly 1 r = 0 ˙
15 14 eqeq2d r = R i = 0 Poly 1 r i = 0 ˙
16 fveq2 r = R Monic 1p r = Monic 1p R
17 16 6 eqtr4di r = R Monic 1p r = M
18 17 ineq2d r = R i Monic 1p r = i M
19 fveq2 r = R deg 1 r = deg 1 R
20 19 5 eqtr4di r = R deg 1 r = D
21 20 fveq1d r = R deg 1 r g = D g
22 14 difeq2d r = R i 0 Poly 1 r = i 0 ˙
23 20 22 imaeq12d r = R deg 1 r i 0 Poly 1 r = D i 0 ˙
24 23 infeq1d r = R sup deg 1 r i 0 Poly 1 r < = sup D i 0 ˙ <
25 21 24 eqeq12d r = R deg 1 r g = sup deg 1 r i 0 Poly 1 r < D g = sup D i 0 ˙ <
26 18 25 riotaeqbidv r = R ι g i Monic 1p r | deg 1 r g = sup deg 1 r i 0 Poly 1 r < = ι g i M | D g = sup D i 0 ˙ <
27 15 13 26 ifbieq12d r = R if i = 0 Poly 1 r 0 Poly 1 r ι g i Monic 1p r | deg 1 r g = sup deg 1 r i 0 Poly 1 r < = if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ <
28 11 27 mpteq12dv r = R i LIdeal Poly 1 r if i = 0 Poly 1 r 0 Poly 1 r ι g i Monic 1p r | deg 1 r g = sup deg 1 r i 0 Poly 1 r < = i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ <
29 df-ig1p idlGen 1p = r V i LIdeal Poly 1 r if i = 0 Poly 1 r 0 Poly 1 r ι g i Monic 1p r | deg 1 r g = sup deg 1 r i 0 Poly 1 r <
30 28 29 4 mptfvmpt R V idlGen 1p R = i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ <
31 7 30 syl R V idlGen 1p R = i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ <
32 2 31 syl5eq R V G = i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ <
33 32 fveq1d R V G I = i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ < I
34 eqeq1 i = I i = 0 ˙ I = 0 ˙
35 ineq1 i = I i M = 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 sup D i 0 ˙ < = sup D I 0 ˙ <
39 38 eqeq2d i = I D g = sup D i 0 ˙ < D g = sup D I 0 ˙ <
40 35 39 riotaeqbidv i = I ι g i M | D g = sup D i 0 ˙ < = ι g I M | D g = sup D I 0 ˙ <
41 34 40 ifbieq2d i = I if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ < = if I = 0 ˙ 0 ˙ ι g I M | D g = sup D I 0 ˙ <
42 eqid i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ < = i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ <
43 3 fvexi 0 ˙ V
44 riotaex ι g I M | D g = sup D I 0 ˙ < V
45 43 44 ifex if I = 0 ˙ 0 ˙ ι g I M | D g = sup D I 0 ˙ < V
46 41 42 45 fvmpt I U i U if i = 0 ˙ 0 ˙ ι g i M | D g = sup D i 0 ˙ < I = if I = 0 ˙ 0 ˙ ι g I M | D g = sup D I 0 ˙ <
47 33 46 sylan9eq R V I U G I = if I = 0 ˙ 0 ˙ ι g I M | D g = sup D I 0 ˙ <