Proof of Theorem ply1rem
Step | Hyp | Ref
| Expression |
1 | | ply1rem.1 |
. . . . . . . . 9
NzRing |
2 | | nzrring 19261 |
. . . . . . . . 9
NzRing |
3 | 1, 2 | syl 17 |
. . . . . . . 8
|
4 | | ply1rem.4 |
. . . . . . . 8
|
5 | | ply1rem.p |
. . . . . . . . . . 11
Poly1 |
6 | | ply1rem.b |
. . . . . . . . . . 11
|
7 | | ply1rem.k |
. . . . . . . . . . 11
|
8 | | ply1rem.x |
. . . . . . . . . . 11
var1 |
9 | | ply1rem.m |
. . . . . . . . . . 11
|
10 | | ply1rem.a |
. . . . . . . . . . 11
algSc |
11 | | ply1rem.g |
. . . . . . . . . . 11
|
12 | | ply1rem.o |
. . . . . . . . . . 11
eval1 |
13 | | ply1rem.2 |
. . . . . . . . . . 11
|
14 | | ply1rem.3 |
. . . . . . . . . . 11
|
15 | | eqid 2622 |
. . . . . . . . . . 11
Monic1p Monic1p |
16 | | eqid 2622 |
. . . . . . . . . . 11
deg1 deg1 |
17 | | eqid 2622 |
. . . . . . . . . . 11
|
18 | 5, 6, 7, 8, 9, 10,
11, 12, 1, 13, 14, 15, 16, 17 | ply1remlem 23922 |
. . . . . . . . . 10
Monic1p deg1 |
19 | 18 | simp1d 1073 |
. . . . . . . . 9
Monic1p |
20 | | eqid 2622 |
. . . . . . . . . 10
Unic1p Unic1p |
21 | 20, 15 | mon1puc1p 23910 |
. . . . . . . . 9
Monic1p Unic1p |
22 | 3, 19, 21 | syl2anc 693 |
. . . . . . . 8
Unic1p |
23 | | ply1rem.e |
. . . . . . . . 9
rem1p |
24 | 23, 5, 6, 20, 16 | r1pdeglt 23918 |
. . . . . . . 8
Unic1p deg1
deg1 |
25 | 3, 4, 22, 24 | syl3anc 1326 |
. . . . . . 7
deg1 deg1 |
26 | 18 | simp2d 1074 |
. . . . . . 7
deg1 |
27 | 25, 26 | breqtrd 4679 |
. . . . . 6
deg1 |
28 | | 1e0p1 11552 |
. . . . . 6
|
29 | 27, 28 | syl6breq 4694 |
. . . . 5
deg1 |
30 | | 0nn0 11307 |
. . . . . 6
|
31 | | nn0leltp1 11436 |
. . . . . 6
deg1 deg1 deg1 |
32 | 30, 31 | mpan2 707 |
. . . . 5
deg1
deg1 deg1 |
33 | 29, 32 | syl5ibrcom 237 |
. . . 4
deg1 deg1 |
34 | | elsni 4194 |
. . . . . 6
deg1 deg1 |
35 | | 0xr 10086 |
. . . . . . 7
|
36 | | mnfle 11969 |
. . . . . . 7
|
37 | 35, 36 | ax-mp 5 |
. . . . . 6
|
38 | 34, 37 | syl6eqbr 4692 |
. . . . 5
deg1 deg1 |
39 | 38 | a1i 11 |
. . . 4
deg1 deg1
|
40 | 23, 5, 6, 20 | r1pcl 23917 |
. . . . . . 7
Unic1p |
41 | 3, 4, 22, 40 | syl3anc 1326 |
. . . . . 6
|
42 | 16, 5, 6 | deg1cl 23843 |
. . . . . 6
deg1
|
43 | 41, 42 | syl 17 |
. . . . 5
deg1 |
44 | | elun 3753 |
. . . . 5
deg1
deg1
deg1 |
45 | 43, 44 | sylib 208 |
. . . 4
deg1
deg1 |
46 | 33, 39, 45 | mpjaod 396 |
. . 3
deg1 |
47 | 16, 5, 6, 10 | deg1le0 23871 |
. . . 4
deg1 coe1 |
48 | 3, 41, 47 | syl2anc 693 |
. . 3
deg1 coe1 |
49 | 46, 48 | mpbid 222 |
. 2
coe1 |
50 | | eqid 2622 |
. . . . . . . . 9
quot1p quot1p |
51 | | eqid 2622 |
. . . . . . . . 9
|
52 | | eqid 2622 |
. . . . . . . . 9
|
53 | 5, 6, 20, 50, 23, 51, 52 | r1pid 23919 |
. . . . . . . 8
Unic1p quot1p |
54 | 3, 4, 22, 53 | syl3anc 1326 |
. . . . . . 7
quot1p |
55 | 54 | fveq2d 6195 |
. . . . . 6
quot1p |
56 | | eqid 2622 |
. . . . . . . . . 10
s s |
57 | 12, 5, 56, 7 | evl1rhm 19696 |
. . . . . . . . 9
RingHom s |
58 | 13, 57 | syl 17 |
. . . . . . . 8
RingHom s |
59 | | rhmghm 18725 |
. . . . . . . 8
RingHom s
s
|
60 | 58, 59 | syl 17 |
. . . . . . 7
s |
61 | 5 | ply1ring 19618 |
. . . . . . . . 9
|
62 | 3, 61 | syl 17 |
. . . . . . . 8
|
63 | 50, 5, 6, 20 | q1pcl 23915 |
. . . . . . . . 9
Unic1p quot1p |
64 | 3, 4, 22, 63 | syl3anc 1326 |
. . . . . . . 8
quot1p |
65 | 5, 6, 15 | mon1pcl 23904 |
. . . . . . . . 9
Monic1p
|
66 | 19, 65 | syl 17 |
. . . . . . . 8
|
67 | 6, 51 | ringcl 18561 |
. . . . . . . 8
quot1p
quot1p |
68 | 62, 64, 66, 67 | syl3anc 1326 |
. . . . . . 7
quot1p |
69 | | eqid 2622 |
. . . . . . . 8
s s |
70 | 6, 52, 69 | ghmlin 17665 |
. . . . . . 7
s quot1p quot1p quot1p s |
71 | 60, 68, 41, 70 | syl3anc 1326 |
. . . . . 6
quot1p quot1p s |
72 | | eqid 2622 |
. . . . . . 7
s s |
73 | | fvex 6201 |
. . . . . . . . 9
|
74 | 7, 73 | eqeltri 2697 |
. . . . . . . 8
|
75 | 74 | a1i 11 |
. . . . . . 7
|
76 | 6, 72 | rhmf 18726 |
. . . . . . . . 9
RingHom s s |
77 | 58, 76 | syl 17 |
. . . . . . . 8
s |
78 | 77, 68 | ffvelrnd 6360 |
. . . . . . 7
quot1p s |
79 | 77, 41 | ffvelrnd 6360 |
. . . . . . 7
s |
80 | | eqid 2622 |
. . . . . . 7
|
81 | 56, 72, 1, 75, 78, 79, 80, 69 | pwsplusgval 16150 |
. . . . . 6
quot1p s quot1p |
82 | 55, 71, 81 | 3eqtrd 2660 |
. . . . 5
quot1p |
83 | 82 | fveq1d 6193 |
. . . 4
quot1p |
84 | 56, 7, 72, 1, 75, 78 | pwselbas 16149 |
. . . . . . 7
quot1p |
85 | | ffn 6045 |
. . . . . . 7
quot1p quot1p |
86 | 84, 85 | syl 17 |
. . . . . 6
quot1p |
87 | 56, 7, 72, 1, 75, 79 | pwselbas 16149 |
. . . . . . 7
|
88 | | ffn 6045 |
. . . . . . 7
|
89 | 87, 88 | syl 17 |
. . . . . 6
|
90 | | fnfvof 6911 |
. . . . . 6
quot1p
quot1p quot1p |
91 | 86, 89, 75, 14, 90 | syl22anc 1327 |
. . . . 5
quot1p quot1p |
92 | | eqid 2622 |
. . . . . . . . . . 11
s s |
93 | 6, 51, 92 | rhmmul 18727 |
. . . . . . . . . 10
RingHom s quot1p
quot1p quot1p s |
94 | 58, 64, 66, 93 | syl3anc 1326 |
. . . . . . . . 9
quot1p quot1p s |
95 | 77, 64 | ffvelrnd 6360 |
. . . . . . . . . 10
quot1p s |
96 | 77, 66 | ffvelrnd 6360 |
. . . . . . . . . 10
s |
97 | | eqid 2622 |
. . . . . . . . . 10
|
98 | 56, 72, 1, 75, 95, 96, 97, 92 | pwsmulrval 16151 |
. . . . . . . . 9
quot1p s quot1p |
99 | 94, 98 | eqtrd 2656 |
. . . . . . . 8
quot1p quot1p |
100 | 99 | fveq1d 6193 |
. . . . . . 7
quot1p quot1p |
101 | 56, 7, 72, 1, 75, 95 | pwselbas 16149 |
. . . . . . . . 9
quot1p |
102 | | ffn 6045 |
. . . . . . . . 9
quot1p quot1p |
103 | 101, 102 | syl 17 |
. . . . . . . 8
quot1p |
104 | 56, 7, 72, 1, 75, 96 | pwselbas 16149 |
. . . . . . . . 9
|
105 | | ffn 6045 |
. . . . . . . . 9
|
106 | 104, 105 | syl 17 |
. . . . . . . 8
|
107 | | fnfvof 6911 |
. . . . . . . 8
quot1p
quot1p quot1p |
108 | 103, 106,
75, 14, 107 | syl22anc 1327 |
. . . . . . 7
quot1p quot1p |
109 | | snidg 4206 |
. . . . . . . . . . . . 13
|
110 | 14, 109 | syl 17 |
. . . . . . . . . . . 12
|
111 | 18 | simp3d 1075 |
. . . . . . . . . . . 12
|
112 | 110, 111 | eleqtrrd 2704 |
. . . . . . . . . . 11
|
113 | | fniniseg 6338 |
. . . . . . . . . . . 12
|
114 | 106, 113 | syl 17 |
. . . . . . . . . . 11
|
115 | 112, 114 | mpbid 222 |
. . . . . . . . . 10
|
116 | 115 | simprd 479 |
. . . . . . . . 9
|
117 | 116 | oveq2d 6666 |
. . . . . . . 8
quot1p quot1p |
118 | 101, 14 | ffvelrnd 6360 |
. . . . . . . . 9
quot1p |
119 | 7, 97, 17 | ringrz 18588 |
. . . . . . . . 9
quot1p quot1p |
120 | 3, 118, 119 | syl2anc 693 |
. . . . . . . 8
quot1p |
121 | 117, 120 | eqtrd 2656 |
. . . . . . 7
quot1p |
122 | 100, 108,
121 | 3eqtrd 2660 |
. . . . . 6
quot1p |
123 | 122 | oveq1d 6665 |
. . . . 5
quot1p |
124 | | ringgrp 18552 |
. . . . . . 7
|
125 | 3, 124 | syl 17 |
. . . . . 6
|
126 | 87, 14 | ffvelrnd 6360 |
. . . . . 6
|
127 | 7, 80, 17 | grplid 17452 |
. . . . . 6
|
128 | 125, 126,
127 | syl2anc 693 |
. . . . 5
|
129 | 91, 123, 128 | 3eqtrd 2660 |
. . . 4
quot1p |
130 | 49 | fveq2d 6195 |
. . . . . . 7
coe1 |
131 | | eqid 2622 |
. . . . . . . . . . 11
coe1 coe1 |
132 | 131, 6, 5, 7 | coe1f 19581 |
. . . . . . . . . 10
coe1 |
133 | 41, 132 | syl 17 |
. . . . . . . . 9
coe1 |
134 | | ffvelrn 6357 |
. . . . . . . . 9
coe1 coe1 |
135 | 133, 30, 134 | sylancl 694 |
. . . . . . . 8
coe1 |
136 | 12, 5, 7, 10 | evl1sca 19698 |
. . . . . . . 8
coe1
coe1 coe1 |
137 | 13, 135, 136 | syl2anc 693 |
. . . . . . 7
coe1 coe1 |
138 | 130, 137 | eqtrd 2656 |
. . . . . 6
coe1 |
139 | 138 | fveq1d 6193 |
. . . . 5
coe1 |
140 | | fvex 6201 |
. . . . . . 7
coe1 |
141 | 140 | fvconst2 6469 |
. . . . . 6
coe1 coe1 |
142 | 14, 141 | syl 17 |
. . . . 5
coe1 coe1 |
143 | 139, 142 | eqtrd 2656 |
. . . 4
coe1 |
144 | 83, 129, 143 | 3eqtrd 2660 |
. . 3
coe1 |
145 | 144 | fveq2d 6195 |
. 2
coe1 |
146 | 49, 145 | eqtr4d 2659 |
1
|