Step | Hyp | Ref
| Expression |
1 | | fta1glem.5 |
. . . . . . . . . . . . . . . . . 18
|
2 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
s s |
3 | | fta1glem.k |
. . . . . . . . . . . . . . . . . . . . 21
|
4 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
s s |
5 | | fta1g.1 |
. . . . . . . . . . . . . . . . . . . . 21
IDomn |
6 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
7 | 3, 6 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . . . 22
|
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
9 | | isidom 19304 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
IDomn Domn |
10 | 9 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
IDomn |
11 | 5, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
12 | | fta1g.o |
. . . . . . . . . . . . . . . . . . . . . . . . 25
eval1 |
13 | | fta1g.p |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Poly1 |
14 | 12, 13, 2, 3 | evl1rhm 19696 |
. . . . . . . . . . . . . . . . . . . . . . . 24
RingHom s |
15 | 11, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
RingHom s |
16 | | fta1g.b |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
17 | 16, 4 | rhmf 18726 |
. . . . . . . . . . . . . . . . . . . . . . 23
RingHom s s |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
s |
19 | | fta1g.2 |
. . . . . . . . . . . . . . . . . . . . . 22
|
20 | 18, 19 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
s |
21 | 2, 3, 4, 5, 8, 20 | pwselbas 16149 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | 21 | ffnd 6046 |
. . . . . . . . . . . . . . . . . . 19
|
23 | | fniniseg 6338 |
. . . . . . . . . . . . . . . . . . 19
|
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
25 | 1, 24 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
26 | 25 | simprd 479 |
. . . . . . . . . . . . . . . 16
|
27 | | fta1glem.x |
. . . . . . . . . . . . . . . . 17
var1 |
28 | | fta1glem.m |
. . . . . . . . . . . . . . . . 17
|
29 | | fta1glem.a |
. . . . . . . . . . . . . . . . 17
algSc |
30 | | fta1glem.g |
. . . . . . . . . . . . . . . . 17
|
31 | 9 | simprbi 480 |
. . . . . . . . . . . . . . . . . . 19
IDomn Domn |
32 | | domnnzr 19295 |
. . . . . . . . . . . . . . . . . . 19
Domn NzRing |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . 18
IDomn NzRing |
34 | 5, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
NzRing |
35 | 25 | simpld 475 |
. . . . . . . . . . . . . . . . 17
|
36 | | fta1g.w |
. . . . . . . . . . . . . . . . 17
|
37 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
r r |
38 | 13, 16, 3, 27, 28, 29, 30, 12, 34, 11, 35, 19, 36, 37 | facth1 23924 |
. . . . . . . . . . . . . . . 16
r
|
39 | 26, 38 | mpbird 247 |
. . . . . . . . . . . . . . 15
r |
40 | | nzrring 19261 |
. . . . . . . . . . . . . . . . 17
NzRing |
41 | 34, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
|
42 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
Monic1p Monic1p |
43 | | fta1g.d |
. . . . . . . . . . . . . . . . . . 19
deg1 |
44 | 13, 16, 3, 27, 28, 29, 30, 12, 34, 11, 35, 42, 43, 36 | ply1remlem 23922 |
. . . . . . . . . . . . . . . . . 18
Monic1p |
45 | 44 | simp1d 1073 |
. . . . . . . . . . . . . . . . 17
Monic1p |
46 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
Unic1p Unic1p |
47 | 46, 42 | mon1puc1p 23910 |
. . . . . . . . . . . . . . . . 17
Monic1p Unic1p |
48 | 41, 45, 47 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
Unic1p |
49 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
50 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
quot1p quot1p |
51 | 13, 37, 16, 46, 49, 50 | dvdsq1p 23920 |
. . . . . . . . . . . . . . . 16
Unic1p r
quot1p |
52 | 41, 19, 48, 51 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
r
quot1p |
53 | 39, 52 | mpbid 222 |
. . . . . . . . . . . . . 14
quot1p |
54 | 53 | fveq2d 6195 |
. . . . . . . . . . . . 13
quot1p |
55 | 50, 13, 16, 46 | q1pcl 23915 |
. . . . . . . . . . . . . . 15
Unic1p quot1p |
56 | 41, 19, 48, 55 | syl3anc 1326 |
. . . . . . . . . . . . . 14
quot1p |
57 | 13, 16, 42 | mon1pcl 23904 |
. . . . . . . . . . . . . . 15
Monic1p
|
58 | 45, 57 | syl 17 |
. . . . . . . . . . . . . 14
|
59 | | eqid 2622 |
. . . . . . . . . . . . . . 15
s s |
60 | 16, 49, 59 | rhmmul 18727 |
. . . . . . . . . . . . . 14
RingHom s quot1p
quot1p quot1p s |
61 | 15, 56, 58, 60 | syl3anc 1326 |
. . . . . . . . . . . . 13
quot1p quot1p s |
62 | 18, 56 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
quot1p s |
63 | 18, 58 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
s |
64 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
65 | 2, 4, 5, 8, 62, 63, 64, 59 | pwsmulrval 16151 |
. . . . . . . . . . . . 13
quot1p s quot1p |
66 | 54, 61, 65 | 3eqtrd 2660 |
. . . . . . . . . . . 12
quot1p |
67 | 66 | fveq1d 6193 |
. . . . . . . . . . 11
quot1p |
68 | 67 | adantr 481 |
. . . . . . . . . 10
quot1p |
69 | 2, 3, 4, 5, 8, 62 | pwselbas 16149 |
. . . . . . . . . . . . 13
quot1p |
70 | 69 | ffnd 6046 |
. . . . . . . . . . . 12
quot1p |
71 | 70 | adantr 481 |
. . . . . . . . . . 11
quot1p |
72 | 2, 3, 4, 5, 8, 63 | pwselbas 16149 |
. . . . . . . . . . . . 13
|
73 | 72 | ffnd 6046 |
. . . . . . . . . . . 12
|
74 | 73 | adantr 481 |
. . . . . . . . . . 11
|
75 | 7 | a1i 11 |
. . . . . . . . . . 11
|
76 | | simpr 477 |
. . . . . . . . . . 11
|
77 | | fnfvof 6911 |
. . . . . . . . . . 11
quot1p
quot1p quot1p |
78 | 71, 74, 75, 76, 77 | syl22anc 1327 |
. . . . . . . . . 10
quot1p quot1p |
79 | 68, 78 | eqtrd 2656 |
. . . . . . . . 9
quot1p |
80 | 79 | eqeq1d 2624 |
. . . . . . . 8
quot1p |
81 | 5, 31 | syl 17 |
. . . . . . . . . 10
Domn |
82 | 81 | adantr 481 |
. . . . . . . . 9
Domn |
83 | 69 | ffvelrnda 6359 |
. . . . . . . . 9
quot1p |
84 | 72 | ffvelrnda 6359 |
. . . . . . . . 9
|
85 | 3, 64, 36 | domneq0 19297 |
. . . . . . . . 9
Domn quot1p quot1p
quot1p |
86 | 82, 83, 84, 85 | syl3anc 1326 |
. . . . . . . 8
quot1p quot1p |
87 | 80, 86 | bitrd 268 |
. . . . . . 7
quot1p |
88 | 87 | pm5.32da 673 |
. . . . . 6
quot1p |
89 | | andi 911 |
. . . . . 6
quot1p
quot1p |
90 | 88, 89 | syl6bb 276 |
. . . . 5
quot1p |
91 | | fniniseg 6338 |
. . . . . 6
|
92 | 22, 91 | syl 17 |
. . . . 5
|
93 | | elun 3753 |
. . . . . 6
quot1p
quot1p |
94 | | fniniseg 6338 |
. . . . . . . 8
quot1p quot1p
quot1p |
95 | 70, 94 | syl 17 |
. . . . . . 7
quot1p
quot1p |
96 | 44 | simp3d 1075 |
. . . . . . . . 9
|
97 | 96 | eleq2d 2687 |
. . . . . . . 8
|
98 | | fniniseg 6338 |
. . . . . . . . 9
|
99 | 73, 98 | syl 17 |
. . . . . . . 8
|
100 | 97, 99 | bitr3d 270 |
. . . . . . 7
|
101 | 95, 100 | orbi12d 746 |
. . . . . 6
quot1p quot1p |
102 | 93, 101 | syl5bb 272 |
. . . . 5
quot1p
quot1p |
103 | 90, 92, 102 | 3bitr4d 300 |
. . . 4
quot1p |
104 | 103 | eqrdv 2620 |
. . 3
quot1p |
105 | 104 | fveq2d 6195 |
. 2
quot1p |
106 | | fvex 6201 |
. . . . . . . . . 10
quot1p |
107 | 106 | cnvex 7113 |
. . . . . . . . 9
quot1p |
108 | 107 | imaex 7104 |
. . . . . . . 8
quot1p |
109 | 108 | a1i 11 |
. . . . . . 7
quot1p |
110 | | fta1glem.3 |
. . . . . . 7
|
111 | | fta1glem.6 |
. . . . . . . . 9
|
112 | | fta1g.z |
. . . . . . . . . 10
|
113 | | fta1glem.4 |
. . . . . . . . . 10
|
114 | 13, 16, 43, 12, 36, 112, 5, 19, 3, 27, 28, 29, 30, 110, 113, 1 | fta1glem1 23925 |
. . . . . . . . 9
quot1p |
115 | | fveq2 6191 |
. . . . . . . . . . . 12
quot1p quot1p |
116 | 115 | eqeq1d 2624 |
. . . . . . . . . . 11
quot1p quot1p |
117 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
quot1p quot1p |
118 | 117 | cnveqd 5298 |
. . . . . . . . . . . . . 14
quot1p quot1p |
119 | 118 | imaeq1d 5465 |
. . . . . . . . . . . . 13
quot1p quot1p |
120 | 119 | fveq2d 6195 |
. . . . . . . . . . . 12
quot1p quot1p |
121 | 120, 115 | breq12d 4666 |
. . . . . . . . . . 11
quot1p
quot1p quot1p |
122 | 116, 121 | imbi12d 334 |
. . . . . . . . . 10
quot1p quot1p quot1p quot1p |
123 | 122 | rspcv 3305 |
. . . . . . . . 9
quot1p
quot1p quot1p quot1p |
124 | 56, 111, 114, 123 | syl3c 66 |
. . . . . . . 8
quot1p quot1p |
125 | 124, 114 | breqtrd 4679 |
. . . . . . 7
quot1p |
126 | | hashbnd 13123 |
. . . . . . 7
quot1p quot1p quot1p |
127 | 109, 110,
125, 126 | syl3anc 1326 |
. . . . . 6
quot1p |
128 | | snfi 8038 |
. . . . . 6
|
129 | | unfi 8227 |
. . . . . 6
quot1p
quot1p |
130 | 127, 128,
129 | sylancl 694 |
. . . . 5
quot1p |
131 | | hashcl 13147 |
. . . . 5
quot1p quot1p |
132 | 130, 131 | syl 17 |
. . . 4
quot1p |
133 | 132 | nn0red 11352 |
. . 3
quot1p |
134 | | hashcl 13147 |
. . . . . 6
quot1p quot1p |
135 | 127, 134 | syl 17 |
. . . . 5
quot1p |
136 | 135 | nn0red 11352 |
. . . 4
quot1p |
137 | | peano2re 10209 |
. . . 4
quot1p
quot1p |
138 | 136, 137 | syl 17 |
. . 3
quot1p |
139 | | peano2nn0 11333 |
. . . . . 6
|
140 | 110, 139 | syl 17 |
. . . . 5
|
141 | 113, 140 | eqeltrd 2701 |
. . . 4
|
142 | 141 | nn0red 11352 |
. . 3
|
143 | | hashun2 13172 |
. . . . 5
quot1p
quot1p quot1p |
144 | 127, 128,
143 | sylancl 694 |
. . . 4
quot1p quot1p |
145 | | hashsng 13159 |
. . . . . 6
|
146 | 1, 145 | syl 17 |
. . . . 5
|
147 | 146 | oveq2d 6666 |
. . . 4
quot1p quot1p |
148 | 144, 147 | breqtrd 4679 |
. . 3
quot1p quot1p |
149 | 110 | nn0red 11352 |
. . . . 5
|
150 | | 1red 10055 |
. . . . 5
|
151 | 136, 149,
150, 125 | leadd1dd 10641 |
. . . 4
quot1p
|
152 | 151, 113 | breqtrrd 4681 |
. . 3
quot1p |
153 | 133, 138,
142, 148, 152 | letrd 10194 |
. 2
quot1p |
154 | 105, 153 | eqbrtrd 4675 |
1
|