Step | Hyp | Ref
| Expression |
1 | | ig1pval.g |
. . . 4
idlGen1p   |
2 | | elex 3054 |
. . . . 5
   |
3 | | fveq2 5865 |
. . . . . . . . . 10
 Poly1  Poly1    |
4 | | ig1pval.p |
. . . . . . . . . 10
Poly1   |
5 | 3, 4 | syl6eqr 2503 |
. . . . . . . . 9
 Poly1    |
6 | 5 | fveq2d 5869 |
. . . . . . . 8
 LIdeal Poly1   LIdeal    |
7 | | ig1pval.u |
. . . . . . . 8
LIdeal   |
8 | 6, 7 | syl6eqr 2503 |
. . . . . . 7
 LIdeal Poly1     |
9 | 5 | fveq2d 5869 |
. . . . . . . . . . 11
    Poly1         |
10 | | ig1pval.z |
. . . . . . . . . . 11
     |
11 | 9, 10 | syl6eqr 2503 |
. . . . . . . . . 10
    Poly1    |
12 | 11 | sneqd 3980 |
. . . . . . . . 9
     Poly1      |
13 | 12 | eqeq2d 2461 |
. . . . . . . 8
      Poly1   
   |
14 | | fveq2 5865 |
. . . . . . . . . . 11
 Monic1p  Monic1p    |
15 | | ig1pval.m |
. . . . . . . . . . 11
Monic1p   |
16 | 14, 15 | syl6eqr 2503 |
. . . . . . . . . 10
 Monic1p    |
17 | 16 | ineq2d 3634 |
. . . . . . . . 9
 
Monic1p       |
18 | | fveq2 5865 |
. . . . . . . . . . . 12
 deg1   deg1     |
19 | | ig1pval.d |
. . . . . . . . . . . 12
deg1    |
20 | 18, 19 | syl6eqr 2503 |
. . . . . . . . . . 11
 deg1     |
21 | 20 | fveq1d 5867 |
. . . . . . . . . 10
  deg1            |
22 | 12 | difeq2d 3551 |
. . . . . . . . . . . 12
 
    Poly1         |
23 | 20, 22 | imaeq12d 5169 |
. . . . . . . . . . 11
  deg1          Poly1              |
24 | 23 | infeq1d 7993 |
. . . . . . . . . 10
 inf  deg1          Poly1        inf    
      |
25 | 21, 24 | eqeq12d 2466 |
. . . . . . . . 9
  
deg1      inf 
deg1          Poly1       
    inf    
       |
26 | 17, 25 | riotaeqbidv 6255 |
. . . . . . . 8
    Monic1p    
deg1      inf 
deg1          Poly1                  inf            |
27 | 13, 11, 26 | ifbieq12d 3908 |
. . . . . . 7
       Poly1        Poly1       Monic1p     deg1      inf  deg1          Poly1                      inf             |
28 | 8, 27 | mpteq12dv 4481 |
. . . . . 6
  LIdeal Poly1         Poly1        Poly1       Monic1p     deg1      inf  deg1          Poly1                

      inf              |
29 | | df-ig1p 23084 |
. . . . . 6
idlGen1p
  LIdeal Poly1         Poly1        Poly1       Monic1p     deg1      inf  deg1          Poly1             |
30 | | fvex 5875 |
. . . . . . . 8
LIdeal   |
31 | 7, 30 | eqeltri 2525 |
. . . . . . 7
 |
32 | 31 | mptex 6136 |
. . . . . 6
     

      inf             |
33 | 28, 29, 32 | fvmpt 5948 |
. . . . 5
 idlGen1p               inf              |
34 | 2, 33 | syl 17 |
. . . 4
 idlGen1p               inf              |
35 | 1, 34 | syl5eq 2497 |
. . 3
              inf              |
36 | 35 | fveq1d 5867 |
. 2
           

      inf                 |
37 | | eqeq1 2455 |
. . . 4
     |
38 | | ineq1 3627 |
. . . . 5
 
     |
39 | | difeq1 3544 |
. . . . . . . 8
 
     |
40 | 39 | imaeq2d 5168 |
. . . . . . 7
               |
41 | 40 | infeq1d 7993 |
. . . . . 6
 inf         inf    
      |
42 | 41 | eqeq2d 2461 |
. . . . 5
      inf        
    inf    
       |
43 | 38, 42 | riotaeqbidv 6255 |
. . . 4
          inf                   inf            |
44 | 37, 43 | ifbieq2d 3906 |
. . 3
             inf                       inf             |
45 | | eqid 2451 |
. . 3
     

      inf                 

      inf             |
46 | | fvex 5875 |
. . . . 5
     |
47 | 10, 46 | eqeltri 2525 |
. . . 4
 |
48 | | riotaex 6256 |
. . . 4
         inf           |
49 | 47, 48 | ifex 3949 |
. . 3
    

      inf            |
50 | 44, 45, 49 | fvmpt 5948 |
. 2
               inf    
                      inf             |
51 | 36, 50 | sylan9eq 2505 |
1
 
         

      inf             |