Step | Hyp | Ref
| Expression |
1 | | uc1pval.c |
. 2
Unic1p   |
2 | | fveq2 5879 |
. . . . . . . 8
 Poly1  Poly1    |
3 | | uc1pval.p |
. . . . . . . 8
Poly1   |
4 | 2, 3 | syl6eqr 2523 |
. . . . . . 7
 Poly1    |
5 | 4 | fveq2d 5883 |
. . . . . 6
    Poly1         |
6 | | uc1pval.b |
. . . . . 6
     |
7 | 5, 6 | syl6eqr 2523 |
. . . . 5
    Poly1     |
8 | 4 | fveq2d 5883 |
. . . . . . . 8
    Poly1         |
9 | | uc1pval.z |
. . . . . . . 8
     |
10 | 8, 9 | syl6eqr 2523 |
. . . . . . 7
    Poly1    |
11 | 10 | neeq2d 2703 |
. . . . . 6
     Poly1     |
12 | | fveq2 5879 |
. . . . . . . . . 10
 deg1   deg1     |
13 | | uc1pval.d |
. . . . . . . . . 10
deg1    |
14 | 12, 13 | syl6eqr 2523 |
. . . . . . . . 9
 deg1     |
15 | 14 | fveq1d 5881 |
. . . . . . . 8
  deg1            |
16 | 15 | fveq2d 5883 |
. . . . . . 7
  coe1    
deg1        coe1           |
17 | | fveq2 5879 |
. . . . . . . 8
 Unit  Unit    |
18 | | uc1pval.u |
. . . . . . . 8
Unit   |
19 | 17, 18 | syl6eqr 2523 |
. . . . . . 7
 Unit    |
20 | 16, 19 | eleq12d 2543 |
. . . . . 6
   coe1    
deg1       Unit   coe1            |
21 | 11, 20 | anbi12d 725 |
. . . . 5
      Poly1    coe1     deg1       Unit  
  coe1             |
22 | 7, 21 | rabeqbidv 3026 |
. . . 4
     Poly1       Poly1    coe1     deg1       Unit       coe1             |
23 | | df-uc1p 23160 |
. . . 4
Unic1p      Poly1       Poly1    coe1     deg1       Unit      |
24 | | fvex 5889 |
. . . . . 6
     |
25 | 6, 24 | eqeltri 2545 |
. . . . 5
 |
26 | 25 | rabex 4550 |
. . . 4
   coe1            |
27 | 22, 23, 26 | fvmpt 5963 |
. . 3
 Unic1p     coe1             |
28 | | fvprc 5873 |
. . . 4
 Unic1p    |
29 | | ssrab2 3500 |
. . . . . 6
   coe1          
 |
30 | | fvprc 5873 |
. . . . . . . . . 10
 Poly1    |
31 | 3, 30 | syl5eq 2517 |
. . . . . . . . 9
   |
32 | 31 | fveq2d 5883 |
. . . . . . . 8
           |
33 | | base0 15240 |
. . . . . . . 8
     |
34 | 32, 33 | syl6eqr 2523 |
. . . . . . 7
       |
35 | 6, 34 | syl5eq 2517 |
. . . . . 6
   |
36 | 29, 35 | syl5sseq 3466 |
. . . . 5
    coe1          
  |
37 | | ss0 3768 |
. . . . 5
    coe1          
   coe1             |
38 | 36, 37 | syl 17 |
. . . 4
    coe1             |
39 | 28, 38 | eqtr4d 2508 |
. . 3
 Unic1p     coe1             |
40 | 27, 39 | pm2.61i 169 |
. 2
Unic1p     coe1            |
41 | 1, 40 | eqtri 2493 |
1
 
 coe1            |