Detailed syntax breakdown of Definition df-ig1p
Step | Hyp | Ref
| Expression |
1 | | cig1p 21719 |
. 2
idlGen1p |
2 | | vr |
. . 3
 |
3 | | cvv 3070 |
. . 3
 |
4 | | vi |
. . . 4
 |
5 | 2 | cv 1369 |
. . . . . 6
 |
6 | | cpl1 17742 |
. . . . . 6
Poly1 |
7 | 5, 6 | cfv 5518 |
. . . . 5
Poly1   |
8 | | clidl 17359 |
. . . . 5
LIdeal |
9 | 7, 8 | cfv 5518 |
. . . 4
LIdeal Poly1    |
10 | 4 | cv 1369 |
. . . . . 6
 |
11 | | c0g 14482 |
. . . . . . . 8
 |
12 | 7, 11 | cfv 5518 |
. . . . . . 7
   Poly1    |
13 | 12 | csn 3977 |
. . . . . 6
    Poly1     |
14 | 10, 13 | wceq 1370 |
. . . . 5
    Poly1     |
15 | | vg |
. . . . . . . . 9
 |
16 | 15 | cv 1369 |
. . . . . . . 8
 |
17 | | cdg1 21641 |
. . . . . . . . 9
deg1 |
18 | 5, 17 | cfv 5518 |
. . . . . . . 8
deg1    |
19 | 16, 18 | cfv 5518 |
. . . . . . 7
 deg1       |
20 | 10, 13 | cdif 3425 |
. . . . . . . . 9
     Poly1      |
21 | 18, 20 | cima 4943 |
. . . . . . . 8
 deg1     
    Poly1       |
22 | | cr 9384 |
. . . . . . . 8
 |
23 | | clt 9521 |
. . . . . . . . 9
 |
24 | 23 | ccnv 4939 |
. . . . . . . 8
 |
25 | 21, 22, 24 | csup 7793 |
. . . . . . 7
  
deg1          Poly1       
 |
26 | 19, 25 | wceq 1370 |
. . . . . 6
 deg1        
deg1          Poly1       
 |
27 | | cmn1 21715 |
. . . . . . . 8
Monic1p |
28 | 5, 27 | cfv 5518 |
. . . . . . 7
Monic1p   |
29 | 10, 28 | cin 3427 |
. . . . . 6
 Monic1p    |
30 | 26, 15, 29 | crio 6152 |
. . . . 5
   Monic1p    
deg1         deg1          Poly1          |
31 | 14, 12, 30 | cif 3891 |
. . . 4
      Poly1        Poly1       Monic1p     deg1        
deg1          Poly1       
   |
32 | 4, 9, 31 | cmpt 4450 |
. . 3
 LIdeal Poly1         Poly1        Poly1       Monic1p     deg1        
deg1          Poly1       
    |
33 | 2, 3, 32 | cmpt 4450 |
. 2
  LIdeal Poly1         Poly1        Poly1       Monic1p     deg1        
deg1          Poly1       
     |
34 | 1, 33 | wceq 1370 |
1
idlGen1p
  LIdeal Poly1         Poly1        Poly1       Monic1p     deg1        
deg1          Poly1       
     |