Proof of Theorem idomrootle
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
Poly1 Poly1 |
2 | | eqid 2622 |
. . 3
Poly1 Poly1 |
3 | | eqid 2622 |
. . 3
deg1 deg1 |
4 | | eqid 2622 |
. . 3
eval1 eval1 |
5 | | eqid 2622 |
. . 3
|
6 | | eqid 2622 |
. . 3
Poly1 Poly1 |
7 | | simp1 1061 |
. . 3
IDomn
IDomn |
8 | | isidom 19304 |
. . . . . . . . 9
IDomn Domn |
9 | 8 | simplbi 476 |
. . . . . . . 8
IDomn |
10 | 7, 9 | syl 17 |
. . . . . . 7
IDomn
|
11 | | crngring 18558 |
. . . . . . 7
|
12 | 10, 11 | syl 17 |
. . . . . 6
IDomn
|
13 | 1 | ply1ring 19618 |
. . . . . 6
Poly1 |
14 | 12, 13 | syl 17 |
. . . . 5
IDomn
Poly1 |
15 | | ringgrp 18552 |
. . . . 5
Poly1 Poly1 |
16 | 14, 15 | syl 17 |
. . . 4
IDomn
Poly1 |
17 | | eqid 2622 |
. . . . . . . 8
mulGrpPoly1 mulGrpPoly1 |
18 | 17 | ringmgp 18553 |
. . . . . . 7
Poly1 mulGrpPoly1 |
19 | 14, 18 | syl 17 |
. . . . . 6
IDomn
mulGrpPoly1 |
20 | | mndmgm 17300 |
. . . . . 6
mulGrpPoly1 mulGrpPoly1 Mgm |
21 | 19, 20 | syl 17 |
. . . . 5
IDomn
mulGrpPoly1 Mgm |
22 | | simp3 1063 |
. . . . 5
IDomn
|
23 | | eqid 2622 |
. . . . . . 7
var1 var1 |
24 | 23, 1, 2 | vr1cl 19587 |
. . . . . 6
var1 Poly1 |
25 | 12, 24 | syl 17 |
. . . . 5
IDomn
var1 Poly1 |
26 | 17, 2 | mgpbas 18495 |
. . . . . 6
Poly1 mulGrpPoly1 |
27 | | eqid 2622 |
. . . . . 6
.gmulGrpPoly1 .gmulGrpPoly1 |
28 | 26, 27 | mulgnncl 17556 |
. . . . 5
mulGrpPoly1 Mgm
var1 Poly1 .gmulGrpPoly1var1 Poly1 |
29 | 21, 22, 25, 28 | syl3anc 1326 |
. . . 4
IDomn
.gmulGrpPoly1var1 Poly1 |
30 | | eqid 2622 |
. . . . . . 7
algScPoly1 algScPoly1 |
31 | | idomrootle.b |
. . . . . . 7
|
32 | 1, 30, 31, 2 | ply1sclf 19655 |
. . . . . 6
algScPoly1Poly1 |
33 | 12, 32 | syl 17 |
. . . . 5
IDomn
algScPoly1Poly1 |
34 | | simp2 1062 |
. . . . 5
IDomn
|
35 | 33, 34 | ffvelrnd 6360 |
. . . 4
IDomn
algScPoly1 Poly1 |
36 | | eqid 2622 |
. . . . 5
Poly1 Poly1 |
37 | 2, 36 | grpsubcl 17495 |
. . . 4
Poly1
.gmulGrpPoly1var1 Poly1 algScPoly1 Poly1
.gmulGrpPoly1var1Poly1algScPoly1 Poly1 |
38 | 16, 29, 35, 37 | syl3anc 1326 |
. . 3
IDomn
.gmulGrpPoly1var1Poly1algScPoly1 Poly1 |
39 | 3, 1, 2 | deg1xrcl 23842 |
. . . . . . . . . 10
algScPoly1 Poly1 deg1 algScPoly1 |
40 | 35, 39 | syl 17 |
. . . . . . . . 9
IDomn
deg1 algScPoly1 |
41 | | 0xr 10086 |
. . . . . . . . . 10
|
42 | 41 | a1i 11 |
. . . . . . . . 9
IDomn
|
43 | | nnre 11027 |
. . . . . . . . . . 11
|
44 | 43 | rexrd 10089 |
. . . . . . . . . 10
|
45 | 44 | 3ad2ant3 1084 |
. . . . . . . . 9
IDomn
|
46 | 3, 1, 31, 30 | deg1sclle 23872 |
. . . . . . . . . 10
deg1 algScPoly1 |
47 | 12, 34, 46 | syl2anc 693 |
. . . . . . . . 9
IDomn
deg1 algScPoly1 |
48 | | nngt0 11049 |
. . . . . . . . . 10
|
49 | 48 | 3ad2ant3 1084 |
. . . . . . . . 9
IDomn
|
50 | 40, 42, 45, 47, 49 | xrlelttrd 11991 |
. . . . . . . 8
IDomn
deg1 algScPoly1 |
51 | 8 | simprbi 480 |
. . . . . . . . . . 11
IDomn Domn |
52 | | domnnzr 19295 |
. . . . . . . . . . 11
Domn NzRing |
53 | 51, 52 | syl 17 |
. . . . . . . . . 10
IDomn NzRing |
54 | 7, 53 | syl 17 |
. . . . . . . . 9
IDomn
NzRing |
55 | | nnnn0 11299 |
. . . . . . . . . 10
|
56 | 55 | 3ad2ant3 1084 |
. . . . . . . . 9
IDomn
|
57 | 3, 1, 23, 17, 27 | deg1pw 23880 |
. . . . . . . . 9
NzRing
deg1 .gmulGrpPoly1var1 |
58 | 54, 56, 57 | syl2anc 693 |
. . . . . . . 8
IDomn
deg1 .gmulGrpPoly1var1 |
59 | 50, 58 | breqtrrd 4681 |
. . . . . . 7
IDomn
deg1 algScPoly1 deg1 .gmulGrpPoly1var1 |
60 | 1, 3, 12, 2, 36, 29, 35, 59 | deg1sub 23868 |
. . . . . 6
IDomn
deg1 .gmulGrpPoly1var1Poly1algScPoly1 deg1 .gmulGrpPoly1var1 |
61 | 60, 58 | eqtrd 2656 |
. . . . 5
IDomn
deg1 .gmulGrpPoly1var1Poly1algScPoly1 |
62 | 61, 56 | eqeltrd 2701 |
. . . 4
IDomn
deg1 .gmulGrpPoly1var1Poly1algScPoly1 |
63 | 3, 1, 6, 2 | deg1nn0clb 23850 |
. . . . 5
.gmulGrpPoly1var1Poly1algScPoly1 Poly1 .gmulGrpPoly1var1Poly1algScPoly1 Poly1
deg1 .gmulGrpPoly1var1Poly1algScPoly1 |
64 | 12, 38, 63 | syl2anc 693 |
. . . 4
IDomn
.gmulGrpPoly1var1Poly1algScPoly1 Poly1
deg1 .gmulGrpPoly1var1Poly1algScPoly1 |
65 | 62, 64 | mpbird 247 |
. . 3
IDomn
.gmulGrpPoly1var1Poly1algScPoly1 Poly1 |
66 | 1, 2, 3, 4, 5, 6, 7, 38, 65 | fta1g 23927 |
. 2
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1
deg1 .gmulGrpPoly1var1Poly1algScPoly1 |
67 | | eqid 2622 |
. . . . . . 7
s s |
68 | | eqid 2622 |
. . . . . . 7
s s |
69 | | fvex 6201 |
. . . . . . . . 9
|
70 | 31, 69 | eqeltri 2697 |
. . . . . . . 8
|
71 | 70 | a1i 11 |
. . . . . . 7
IDomn
|
72 | 4, 1, 67, 31 | evl1rhm 19696 |
. . . . . . . . . 10
eval1 Poly1 RingHom s |
73 | 10, 72 | syl 17 |
. . . . . . . . 9
IDomn
eval1 Poly1 RingHom s |
74 | 2, 68 | rhmf 18726 |
. . . . . . . . 9
eval1 Poly1 RingHom s eval1Poly1 s |
75 | 73, 74 | syl 17 |
. . . . . . . 8
IDomn
eval1Poly1 s |
76 | 75, 38 | ffvelrnd 6360 |
. . . . . . 7
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 s |
77 | 67, 31, 68, 7, 71, 76 | pwselbas 16149 |
. . . . . 6
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
78 | | ffn 6045 |
. . . . . 6
eval1.gmulGrpPoly1var1Poly1algScPoly1 eval1.gmulGrpPoly1var1Poly1algScPoly1 |
79 | 77, 78 | syl 17 |
. . . . 5
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
80 | | fniniseg2 6340 |
. . . . 5
eval1.gmulGrpPoly1var1Poly1algScPoly1 eval1.gmulGrpPoly1var1Poly1algScPoly1 eval1.gmulGrpPoly1var1Poly1algScPoly1 |
81 | 79, 80 | syl 17 |
. . . 4
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 eval1.gmulGrpPoly1var1Poly1algScPoly1 |
82 | 10 | adantr 481 |
. . . . . . . . 9
IDomn
|
83 | | simpr 477 |
. . . . . . . . 9
IDomn
|
84 | 4, 23, 31, 1, 2, 82, 83 | evl1vard 19701 |
. . . . . . . . . 10
IDomn
var1 Poly1 eval1var1 |
85 | | idomrootle.e |
. . . . . . . . . 10
.gmulGrp |
86 | | simpl3 1066 |
. . . . . . . . . . 11
IDomn
|
87 | 86, 55 | syl 17 |
. . . . . . . . . 10
IDomn
|
88 | 4, 1, 31, 2, 82, 83, 84, 27, 85, 87 | evl1expd 19709 |
. . . . . . . . 9
IDomn
.gmulGrpPoly1var1 Poly1 eval1.gmulGrpPoly1var1 |
89 | | simpl2 1065 |
. . . . . . . . . 10
IDomn
|
90 | 4, 1, 31, 30, 2, 82, 89, 83 | evl1scad 19699 |
. . . . . . . . 9
IDomn
algScPoly1 Poly1 eval1algScPoly1 |
91 | | eqid 2622 |
. . . . . . . . 9
|
92 | 4, 1, 31, 2, 82, 83, 88, 90, 36, 91 | evl1subd 19706 |
. . . . . . . 8
IDomn
.gmulGrpPoly1var1Poly1algScPoly1 Poly1 eval1.gmulGrpPoly1var1Poly1algScPoly1 |
93 | 92 | simprd 479 |
. . . . . . 7
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
94 | 93 | eqeq1d 2624 |
. . . . . 6
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
95 | | ringgrp 18552 |
. . . . . . . . 9
|
96 | 12, 95 | syl 17 |
. . . . . . . 8
IDomn
|
97 | 96 | adantr 481 |
. . . . . . 7
IDomn
|
98 | | eqid 2622 |
. . . . . . . . . . . 12
mulGrp mulGrp |
99 | 98 | ringmgp 18553 |
. . . . . . . . . . 11
mulGrp |
100 | 12, 99 | syl 17 |
. . . . . . . . . 10
IDomn
mulGrp |
101 | 100 | adantr 481 |
. . . . . . . . 9
IDomn
mulGrp |
102 | | mndmgm 17300 |
. . . . . . . . 9
mulGrp mulGrp Mgm |
103 | 101, 102 | syl 17 |
. . . . . . . 8
IDomn
mulGrp Mgm |
104 | 98, 31 | mgpbas 18495 |
. . . . . . . . 9
mulGrp |
105 | 104, 85 | mulgnncl 17556 |
. . . . . . . 8
mulGrp Mgm |
106 | 103, 86, 83, 105 | syl3anc 1326 |
. . . . . . 7
IDomn
|
107 | 31, 5, 91 | grpsubeq0 17501 |
. . . . . . 7
|
108 | 97, 106, 89, 107 | syl3anc 1326 |
. . . . . 6
IDomn
|
109 | 94, 108 | bitrd 268 |
. . . . 5
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
110 | 109 | rabbidva 3188 |
. . . 4
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
111 | 81, 110 | eqtrd 2656 |
. . 3
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
112 | 111 | fveq2d 6195 |
. 2
IDomn
eval1.gmulGrpPoly1var1Poly1algScPoly1 |
113 | 66, 112, 61 | 3brtr3d 4684 |
1
IDomn
|