Proof of Theorem idomrootle
Step | Hyp | Ref
| Expression |
1 | | eqid 2404 |
. . 3
Poly1  Poly1   |
2 | | eqid 2404 |
. . 3
   Poly1      Poly1    |
3 | | eqid 2404 |
. . 3
deg1   deg1    |
4 | | eqid 2404 |
. . 3
eval1  eval1   |
5 | | eqid 2404 |
. . 3
         |
6 | | eqid 2404 |
. . 3
   Poly1      Poly1    |
7 | | simp1 957 |
. . 3
  IDomn
 IDomn |
8 | | isidom 16319 |
. . . . . . . . 9
 IDomn  Domn  |
9 | 8 | simplbi 447 |
. . . . . . . 8
 IDomn   |
10 | 7, 9 | syl 16 |
. . . . . . 7
  IDomn
   |
11 | | crngrng 15629 |
. . . . . . 7

  |
12 | 10, 11 | syl 16 |
. . . . . 6
  IDomn
   |
13 | 1 | ply1rng 16597 |
. . . . . 6

Poly1    |
14 | 12, 13 | syl 16 |
. . . . 5
  IDomn
 Poly1    |
15 | | rnggrp 15624 |
. . . . 5
 Poly1  Poly1    |
16 | 14, 15 | syl 16 |
. . . 4
  IDomn
 Poly1    |
17 | | eqid 2404 |
. . . . . . 7
mulGrp Poly1   mulGrp Poly1    |
18 | 17 | rngmgp 15625 |
. . . . . 6
 Poly1  mulGrp Poly1     |
19 | 14, 18 | syl 16 |
. . . . 5
  IDomn
 mulGrp Poly1     |
20 | | simp3 959 |
. . . . 5
  IDomn
   |
21 | | eqid 2404 |
. . . . . . 7
var1  var1   |
22 | 21, 1, 2 | vr1cl 16566 |
. . . . . 6

var1     Poly1     |
23 | 12, 22 | syl 16 |
. . . . 5
  IDomn
 var1     Poly1     |
24 | 17, 2 | mgpbas 15609 |
. . . . . 6
   Poly1      mulGrp Poly1     |
25 | | eqid 2404 |
. . . . . 6
.g mulGrp Poly1    .g mulGrp Poly1     |
26 | 24, 25 | mulgnncl 14860 |
. . . . 5
  mulGrp Poly1   var1     Poly1      .g mulGrp Poly1     var1      Poly1     |
27 | 19, 20, 23, 26 | syl3anc 1184 |
. . . 4
  IDomn
   .g mulGrp Poly1     var1      Poly1     |
28 | | eqid 2404 |
. . . . . . 7
algSc Poly1   algSc Poly1    |
29 | | idomrootle.b |
. . . . . . 7
     |
30 | 1, 28, 29, 2 | ply1sclf 16632 |
. . . . . 6

algSc Poly1          Poly1     |
31 | 12, 30 | syl 16 |
. . . . 5
  IDomn
 algSc Poly1          Poly1     |
32 | | simp2 958 |
. . . . 5
  IDomn
   |
33 | 31, 32 | ffvelrnd 5830 |
. . . 4
  IDomn
  algSc Poly1         Poly1     |
34 | | eqid 2404 |
. . . . 5
   Poly1      Poly1    |
35 | 2, 34 | grpsubcl 14824 |
. . . 4
  Poly1 
  .g mulGrp Poly1     var1      Poly1    algSc Poly1         Poly1   
   .g mulGrp Poly1     var1       Poly1     algSc Poly1          Poly1     |
36 | 16, 27, 33, 35 | syl3anc 1184 |
. . 3
  IDomn
    .g mulGrp Poly1     var1       Poly1     algSc Poly1          Poly1     |
37 | 3, 1, 2 | deg1xrcl 19958 |
. . . . . . . . . 10
  algSc Poly1         Poly1    deg1      algSc Poly1         |
38 | 33, 37 | syl 16 |
. . . . . . . . 9
  IDomn
  deg1      algSc Poly1         |
39 | | 0xr 9087 |
. . . . . . . . . 10
 |
40 | 39 | a1i 11 |
. . . . . . . . 9
  IDomn
   |
41 | | nnre 9963 |
. . . . . . . . . . 11
   |
42 | 41 | rexrd 9090 |
. . . . . . . . . 10
   |
43 | 42 | 3ad2ant3 980 |
. . . . . . . . 9
  IDomn
   |
44 | 3, 1, 29, 28 | deg1sclle 19988 |
. . . . . . . . . 10
    deg1      algSc Poly1         |
45 | 12, 32, 44 | syl2anc 643 |
. . . . . . . . 9
  IDomn
  deg1      algSc Poly1         |
46 | | nngt0 9985 |
. . . . . . . . . 10
   |
47 | 46 | 3ad2ant3 980 |
. . . . . . . . 9
  IDomn
   |
48 | 38, 40, 43, 45, 47 | xrlelttrd 10706 |
. . . . . . . 8
  IDomn
  deg1      algSc Poly1         |
49 | 8 | simprbi 451 |
. . . . . . . . . . 11
 IDomn Domn |
50 | | domnnzr 16310 |
. . . . . . . . . . 11
 Domn NzRing |
51 | 49, 50 | syl 16 |
. . . . . . . . . 10
 IDomn NzRing |
52 | 7, 51 | syl 16 |
. . . . . . . . 9
  IDomn
 NzRing |
53 | | nnnn0 10184 |
. . . . . . . . . 10
   |
54 | 53 | 3ad2ant3 980 |
. . . . . . . . 9
  IDomn
   |
55 | 3, 1, 21, 17, 25 | deg1pw 19996 |
. . . . . . . . 9
  NzRing
  deg1       .g mulGrp Poly1     var1      |
56 | 52, 54, 55 | syl2anc 643 |
. . . . . . . 8
  IDomn
  deg1       .g mulGrp Poly1     var1      |
57 | 48, 56 | breqtrrd 4198 |
. . . . . . 7
  IDomn
  deg1      algSc Poly1        deg1       .g mulGrp Poly1     var1      |
58 | 1, 3, 12, 2, 34, 27, 33, 57 | deg1sub 19984 |
. . . . . 6
  IDomn
  deg1        .g mulGrp Poly1     var1       Poly1     algSc Poly1         deg1       .g mulGrp Poly1     var1      |
59 | 58, 56 | eqtrd 2436 |
. . . . 5
  IDomn
  deg1        .g mulGrp Poly1     var1       Poly1     algSc Poly1          |
60 | 59, 54 | eqeltrd 2478 |
. . . 4
  IDomn
  deg1        .g mulGrp Poly1     var1       Poly1     algSc Poly1          |
61 | 3, 1, 6, 2 | deg1nn0clb 19966 |
. . . . 5
     .g mulGrp Poly1     var1       Poly1     algSc Poly1          Poly1        .g mulGrp Poly1     var1       Poly1     algSc Poly1          Poly1   
deg1        .g mulGrp Poly1     var1       Poly1     algSc Poly1           |
62 | 12, 36, 61 | syl2anc 643 |
. . . 4
  IDomn
     .g mulGrp Poly1     var1       Poly1     algSc Poly1          Poly1  
 deg1        .g mulGrp Poly1     var1       Poly1     algSc Poly1           |
63 | 60, 62 | mpbird 224 |
. . 3
  IDomn
    .g mulGrp Poly1     var1       Poly1     algSc Poly1          Poly1     |
64 | 1, 2, 3, 4, 5, 6, 7, 36, 63 | fta1g 20043 |
. 2
  IDomn
       eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                  
deg1        .g mulGrp Poly1     var1       Poly1     algSc Poly1          |
65 | | eqid 2404 |
. . . . . . 7
 s   s   |
66 | | eqid 2404 |
. . . . . . 7
    s       s    |
67 | | fvex 5701 |
. . . . . . . . 9
     |
68 | 29, 67 | eqeltri 2474 |
. . . . . . . 8
 |
69 | 68 | a1i 11 |
. . . . . . 7
  IDomn
   |
70 | 4, 1, 65, 29 | evl1rhm 19902 |
. . . . . . . . . 10

eval1   Poly1  RingHom  s     |
71 | 10, 70 | syl 16 |
. . . . . . . . 9
  IDomn
 eval1   Poly1  RingHom  s     |
72 | 2, 66 | rhmf 15782 |
. . . . . . . . 9
 eval1   Poly1  RingHom  s   eval1       Poly1         s     |
73 | 71, 72 | syl 16 |
. . . . . . . 8
  IDomn
 eval1       Poly1         s     |
74 | 73, 36 | ffvelrnd 5830 |
. . . . . . 7
  IDomn
  eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1            s     |
75 | 65, 29, 66, 7, 69, 74 | pwselbas 13666 |
. . . . . 6
  IDomn
  eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1              |
76 | | ffn 5550 |
. . . . . 6
  eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1             eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1          |
77 | 75, 76 | syl 16 |
. . . . 5
  IDomn
  eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1          |
78 | | fniniseg2 5812 |
. . . . 5
  eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1           eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                    eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                  |
79 | 77, 78 | syl 16 |
. . . 4
  IDomn
    eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                    eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                  |
80 | 10 | adantr 452 |
. . . . . . . . 9
   IDomn
    |
81 | | simpr 448 |
. . . . . . . . 9
   IDomn
    |
82 | 4, 21, 29, 1, 2, 80, 81 | evl1vard 19906 |
. . . . . . . . . 10
   IDomn
   var1     Poly1     eval1    var1         |
83 | | idomrootle.e |
. . . . . . . . . 10
.g mulGrp    |
84 | | simpl3 962 |
. . . . . . . . . . 11
   IDomn
    |
85 | 84, 53 | syl 16 |
. . . . . . . . . 10
   IDomn
    |
86 | 4, 1, 29, 2, 80, 81, 82, 25, 83, 85 | evl1expd 19911 |
. . . . . . . . 9
   IDomn
     .g mulGrp Poly1     var1      Poly1     eval1      .g mulGrp Poly1     var1            |
87 | | simpl2 961 |
. . . . . . . . . 10
   IDomn
    |
88 | 4, 1, 29, 28, 2, 80, 87, 81 | evl1scad 19904 |
. . . . . . . . 9
   IDomn
    algSc Poly1         Poly1     eval1     algSc Poly1             |
89 | | eqid 2404 |
. . . . . . . . 9
         |
90 | 4, 1, 29, 2, 80, 81, 86, 88, 34, 89 | evl1subd 19908 |
. . . . . . . 8
   IDomn
      .g mulGrp Poly1     var1       Poly1     algSc Poly1          Poly1     eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                        |
91 | 90 | simprd 450 |
. . . . . . 7
   IDomn
    eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                       |
92 | 91 | eqeq1d 2412 |
. . . . . 6
   IDomn
     eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                                |
93 | | rnggrp 15624 |
. . . . . . . . 9

  |
94 | 12, 93 | syl 16 |
. . . . . . . 8
  IDomn
   |
95 | 94 | adantr 452 |
. . . . . . 7
   IDomn
    |
96 | | eqid 2404 |
. . . . . . . . . . 11
mulGrp  mulGrp   |
97 | 96 | rngmgp 15625 |
. . . . . . . . . 10

mulGrp    |
98 | 12, 97 | syl 16 |
. . . . . . . . 9
  IDomn
 mulGrp    |
99 | 98 | adantr 452 |
. . . . . . . 8
   IDomn
  mulGrp    |
100 | 96, 29 | mgpbas 15609 |
. . . . . . . . 9
   mulGrp    |
101 | 100, 83 | mulgnncl 14860 |
. . . . . . . 8
  mulGrp       |
102 | 99, 84, 81, 101 | syl3anc 1184 |
. . . . . . 7
   IDomn
      |
103 | 29, 5, 89 | grpsubeq0 14830 |
. . . . . . 7
  
                
     |
104 | 95, 102, 87, 103 | syl3anc 1184 |
. . . . . 6
   IDomn
                
     |
105 | 92, 104 | bitrd 245 |
. . . . 5
   IDomn
     eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                    |
106 | 105 | rabbidva 2907 |
. . . 4
  IDomn
    eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                      |
107 | 79, 106 | eqtrd 2436 |
. . 3
  IDomn
    eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                       |
108 | 107 | fveq2d 5691 |
. 2
  IDomn
       eval1       .g mulGrp Poly1     var1       Poly1     algSc Poly1                            |
109 | 64, 108, 59 | 3brtr3d 4201 |
1
  IDomn
           |