Step | Hyp | Ref
| Expression |
1 | | ig1pval.g |
. . . 4
idlGen1p |
2 | | elex 3212 |
. . . . 5
|
3 | | fveq2 6191 |
. . . . . . . . . 10
Poly1 Poly1 |
4 | | ig1pval.p |
. . . . . . . . . 10
Poly1 |
5 | 3, 4 | syl6eqr 2674 |
. . . . . . . . 9
Poly1 |
6 | 5 | fveq2d 6195 |
. . . . . . . 8
LIdealPoly1 LIdeal |
7 | | ig1pval.u |
. . . . . . . 8
LIdeal |
8 | 6, 7 | syl6eqr 2674 |
. . . . . . 7
LIdealPoly1 |
9 | 5 | fveq2d 6195 |
. . . . . . . . . . 11
Poly1 |
10 | | ig1pval.z |
. . . . . . . . . . 11
|
11 | 9, 10 | syl6eqr 2674 |
. . . . . . . . . 10
Poly1 |
12 | 11 | sneqd 4189 |
. . . . . . . . 9
Poly1 |
13 | 12 | eqeq2d 2632 |
. . . . . . . 8
Poly1
|
14 | | fveq2 6191 |
. . . . . . . . . . 11
Monic1p Monic1p |
15 | | ig1pval.m |
. . . . . . . . . . 11
Monic1p |
16 | 14, 15 | syl6eqr 2674 |
. . . . . . . . . 10
Monic1p |
17 | 16 | ineq2d 3814 |
. . . . . . . . 9
Monic1p |
18 | | fveq2 6191 |
. . . . . . . . . . . 12
deg1 deg1 |
19 | | ig1pval.d |
. . . . . . . . . . . 12
deg1 |
20 | 18, 19 | syl6eqr 2674 |
. . . . . . . . . . 11
deg1 |
21 | 20 | fveq1d 6193 |
. . . . . . . . . 10
deg1 |
22 | 12 | difeq2d 3728 |
. . . . . . . . . . . 12
Poly1 |
23 | 20, 22 | imaeq12d 5467 |
. . . . . . . . . . 11
deg1 Poly1 |
24 | 23 | infeq1d 8383 |
. . . . . . . . . 10
inf deg1 Poly1 inf
|
25 | 21, 24 | eqeq12d 2637 |
. . . . . . . . 9
deg1 inf
deg1 Poly1
inf
|
26 | 17, 25 | riotaeqbidv 6614 |
. . . . . . . 8
Monic1p
deg1 inf
deg1 Poly1 inf |
27 | 13, 11, 26 | ifbieq12d 4113 |
. . . . . . 7
Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 inf |
28 | 8, 27 | mpteq12dv 4733 |
. . . . . 6
LIdealPoly1 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1
inf |
29 | | df-ig1p 23894 |
. . . . . 6
idlGen1p
LIdealPoly1 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 |
30 | | fvex 6201 |
. . . . . . . 8
LIdeal |
31 | 7, 30 | eqeltri 2697 |
. . . . . . 7
|
32 | 31 | mptex 6486 |
. . . . . 6
inf |
33 | 28, 29, 32 | fvmpt 6282 |
. . . . 5
idlGen1p inf |
34 | 2, 33 | syl 17 |
. . . 4
idlGen1p inf |
35 | 1, 34 | syl5eq 2668 |
. . 3
inf |
36 | 35 | fveq1d 6193 |
. 2
inf |
37 | | eqeq1 2626 |
. . . 4
|
38 | | ineq1 3807 |
. . . . 5
|
39 | | difeq1 3721 |
. . . . . . . 8
|
40 | 39 | imaeq2d 5466 |
. . . . . . 7
|
41 | 40 | infeq1d 8383 |
. . . . . 6
inf inf
|
42 | 41 | eqeq2d 2632 |
. . . . 5
inf
inf
|
43 | 38, 42 | riotaeqbidv 6614 |
. . . 4
inf inf |
44 | 37, 43 | ifbieq2d 4111 |
. . 3
inf inf |
45 | | eqid 2622 |
. . 3
inf
inf |
46 | | fvex 6201 |
. . . . 5
|
47 | 10, 46 | eqeltri 2697 |
. . . 4
|
48 | | riotaex 6615 |
. . . 4
inf |
49 | 47, 48 | ifex 4156 |
. . 3
inf |
50 | 44, 45, 49 | fvmpt 6282 |
. 2
inf
inf |
51 | 36, 50 | sylan9eq 2676 |
1
inf |