Detailed syntax breakdown of Definition df-ig1p
Step | Hyp | Ref
| Expression |
1 | | cig1p 23889 |
. 2
idlGen1p |
2 | | vr |
. . 3
|
3 | | cvv 3200 |
. . 3
|
4 | | vi |
. . . 4
|
5 | 2 | cv 1482 |
. . . . . 6
|
6 | | cpl1 19547 |
. . . . . 6
Poly1 |
7 | 5, 6 | cfv 5888 |
. . . . 5
Poly1 |
8 | | clidl 19170 |
. . . . 5
LIdeal |
9 | 7, 8 | cfv 5888 |
. . . 4
LIdealPoly1 |
10 | 4 | cv 1482 |
. . . . . 6
|
11 | | c0g 16100 |
. . . . . . . 8
|
12 | 7, 11 | cfv 5888 |
. . . . . . 7
Poly1 |
13 | 12 | csn 4177 |
. . . . . 6
Poly1 |
14 | 10, 13 | wceq 1483 |
. . . . 5
Poly1 |
15 | | vg |
. . . . . . . . 9
|
16 | 15 | cv 1482 |
. . . . . . . 8
|
17 | | cdg1 23814 |
. . . . . . . . 9
deg1 |
18 | 5, 17 | cfv 5888 |
. . . . . . . 8
deg1 |
19 | 16, 18 | cfv 5888 |
. . . . . . 7
deg1 |
20 | 10, 13 | cdif 3571 |
. . . . . . . . 9
Poly1 |
21 | 18, 20 | cima 5117 |
. . . . . . . 8
deg1
Poly1 |
22 | | cr 9935 |
. . . . . . . 8
|
23 | | clt 10074 |
. . . . . . . 8
|
24 | 21, 22, 23 | cinf 8347 |
. . . . . . 7
inf deg1 Poly1 |
25 | 19, 24 | wceq 1483 |
. . . . . 6
deg1 inf deg1 Poly1 |
26 | | cmn1 23885 |
. . . . . . . 8
Monic1p |
27 | 5, 26 | cfv 5888 |
. . . . . . 7
Monic1p |
28 | 10, 27 | cin 3573 |
. . . . . 6
Monic1p |
29 | 25, 15, 28 | crio 6610 |
. . . . 5
Monic1p
deg1 inf
deg1 Poly1 |
30 | 14, 12, 29 | cif 4086 |
. . . 4
Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 |
31 | 4, 9, 30 | cmpt 4729 |
. . 3
LIdealPoly1 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 |
32 | 2, 3, 31 | cmpt 4729 |
. 2
LIdealPoly1 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 |
33 | 1, 32 | wceq 1483 |
1
idlGen1p
LIdealPoly1 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 |