Proof of Theorem fta1blem
Step | Hyp | Ref
| Expression |
1 | | fta1blem.3 |
. . . 4
|
2 | | fta1b.o |
. . . . . . 7
eval1 |
3 | | fta1b.p |
. . . . . . 7
Poly1 |
4 | | fta1blem.k |
. . . . . . 7
|
5 | | fta1b.b |
. . . . . . 7
|
6 | | fta1blem.1 |
. . . . . . 7
|
7 | | fta1blem.x |
. . . . . . . 8
var1 |
8 | 2, 7, 4, 3, 5, 6, 1 | evl1vard 19701 |
. . . . . . 7
|
9 | | fta1blem.2 |
. . . . . . 7
|
10 | | fta1blem.s |
. . . . . . 7
|
11 | | fta1blem.t |
. . . . . . 7
|
12 | 2, 3, 4, 5, 6, 1, 8, 9, 10, 11 | evl1vsd 19708 |
. . . . . 6
|
13 | 12 | simprd 479 |
. . . . 5
|
14 | | fta1blem.4 |
. . . . 5
|
15 | 13, 14 | eqtrd 2656 |
. . . 4
|
16 | | eqid 2622 |
. . . . . . 7
s s |
17 | | eqid 2622 |
. . . . . . 7
s s |
18 | | fvex 6201 |
. . . . . . . . 9
|
19 | 4, 18 | eqeltri 2697 |
. . . . . . . 8
|
20 | 19 | a1i 11 |
. . . . . . 7
|
21 | 2, 3, 16, 4 | evl1rhm 19696 |
. . . . . . . . . 10
RingHom s |
22 | 6, 21 | syl 17 |
. . . . . . . . 9
RingHom s |
23 | 5, 17 | rhmf 18726 |
. . . . . . . . 9
RingHom s s |
24 | 22, 23 | syl 17 |
. . . . . . . 8
s |
25 | 12 | simpld 475 |
. . . . . . . 8
|
26 | 24, 25 | ffvelrnd 6360 |
. . . . . . 7
s |
27 | 16, 4, 17, 6, 20, 26 | pwselbas 16149 |
. . . . . 6
|
28 | 27 | ffnd 6046 |
. . . . 5
|
29 | | fniniseg 6338 |
. . . . 5
|
30 | 28, 29 | syl 17 |
. . . 4
|
31 | 1, 15, 30 | mpbir2and 957 |
. . 3
|
32 | | fvex 6201 |
. . . . . . . 8
|
33 | 32 | cnvex 7113 |
. . . . . . 7
|
34 | 33 | imaex 7104 |
. . . . . 6
|
35 | 34 | a1i 11 |
. . . . 5
|
36 | | 1nn0 11308 |
. . . . . 6
|
37 | 36 | a1i 11 |
. . . . 5
|
38 | | crngring 18558 |
. . . . . . . . . . . . 13
|
39 | 6, 38 | syl 17 |
. . . . . . . . . . . 12
|
40 | 7, 3, 5 | vr1cl 19587 |
. . . . . . . . . . . 12
|
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
|
42 | | eqid 2622 |
. . . . . . . . . . . . 13
mulGrp mulGrp |
43 | 42, 5 | mgpbas 18495 |
. . . . . . . . . . . 12
mulGrp |
44 | | eqid 2622 |
. . . . . . . . . . . 12
.gmulGrp .gmulGrp |
45 | 43, 44 | mulg1 17548 |
. . . . . . . . . . 11
.gmulGrp |
46 | 41, 45 | syl 17 |
. . . . . . . . . 10
.gmulGrp |
47 | 46 | oveq2d 6666 |
. . . . . . . . 9
.gmulGrp |
48 | | fta1blem.5 |
. . . . . . . . . . 11
|
49 | | fta1b.w |
. . . . . . . . . . . . 13
|
50 | 49, 4, 3, 7, 10, 42, 44 | coe1tmfv1 19644 |
. . . . . . . . . . . 12
coe1 .gmulGrp |
51 | 39, 9, 37, 50 | syl3anc 1326 |
. . . . . . . . . . 11
coe1 .gmulGrp |
52 | | fta1b.z |
. . . . . . . . . . . . . . 15
|
53 | 3, 52, 49 | coe1z 19633 |
. . . . . . . . . . . . . 14
coe1
|
54 | 39, 53 | syl 17 |
. . . . . . . . . . . . 13
coe1 |
55 | 54 | fveq1d 6193 |
. . . . . . . . . . . 12
coe1 |
56 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
57 | 49, 56 | eqeltri 2697 |
. . . . . . . . . . . . . 14
|
58 | 57 | fvconst2 6469 |
. . . . . . . . . . . . 13
|
59 | 36, 58 | ax-mp 5 |
. . . . . . . . . . . 12
|
60 | 55, 59 | syl6eq 2672 |
. . . . . . . . . . 11
coe1 |
61 | 48, 51, 60 | 3netr4d 2871 |
. . . . . . . . . 10
coe1 .gmulGrp coe1 |
62 | | fveq2 6191 |
. . . . . . . . . . . 12
.gmulGrp coe1 .gmulGrp coe1 |
63 | 62 | fveq1d 6193 |
. . . . . . . . . . 11
.gmulGrp coe1 .gmulGrp coe1 |
64 | 63 | necon3i 2826 |
. . . . . . . . . 10
coe1 .gmulGrp coe1 .gmulGrp |
65 | 61, 64 | syl 17 |
. . . . . . . . 9
.gmulGrp |
66 | 47, 65 | eqnetrrd 2862 |
. . . . . . . 8
|
67 | | eldifsn 4317 |
. . . . . . . 8
|
68 | 25, 66, 67 | sylanbrc 698 |
. . . . . . 7
|
69 | | fta1blem.6 |
. . . . . . 7
|
70 | 68, 69 | mpd 15 |
. . . . . 6
|
71 | 47 | fveq2d 6195 |
. . . . . . 7
.gmulGrp |
72 | | fta1b.d |
. . . . . . . . 9
deg1 |
73 | 72, 4, 3, 7, 10, 42, 44, 49 | deg1tm 23878 |
. . . . . . . 8
.gmulGrp |
74 | 39, 9, 48, 37, 73 | syl121anc 1331 |
. . . . . . 7
.gmulGrp |
75 | 71, 74 | eqtr3d 2658 |
. . . . . 6
|
76 | 70, 75 | breqtrd 4679 |
. . . . 5
|
77 | | hashbnd 13123 |
. . . . 5
|
78 | 35, 37, 76, 77 | syl3anc 1326 |
. . . 4
|
79 | 4, 49 | ring0cl 18569 |
. . . . . . 7
|
80 | 39, 79 | syl 17 |
. . . . . 6
|
81 | | eqid 2622 |
. . . . . . . . . . . . 13
algSc algSc |
82 | 3, 81, 4, 5 | ply1sclf 19655 |
. . . . . . . . . . . 12
algSc |
83 | 39, 82 | syl 17 |
. . . . . . . . . . 11
algSc |
84 | 83, 9 | ffvelrnd 6360 |
. . . . . . . . . 10
algSc |
85 | | eqid 2622 |
. . . . . . . . . . 11
|
86 | | eqid 2622 |
. . . . . . . . . . 11
s s |
87 | 5, 85, 86 | rhmmul 18727 |
. . . . . . . . . 10
RingHom s algSc
algSc algSc s |
88 | 22, 84, 41, 87 | syl3anc 1326 |
. . . . . . . . 9
algSc algSc s |
89 | 3 | ply1assa 19569 |
. . . . . . . . . . . 12
AssAlg |
90 | 6, 89 | syl 17 |
. . . . . . . . . . 11
AssAlg |
91 | 3 | ply1sca 19623 |
. . . . . . . . . . . . . . 15
Scalar |
92 | 6, 91 | syl 17 |
. . . . . . . . . . . . . 14
Scalar |
93 | 92 | fveq2d 6195 |
. . . . . . . . . . . . 13
Scalar |
94 | 4, 93 | syl5eq 2668 |
. . . . . . . . . . . 12
Scalar |
95 | 9, 94 | eleqtrd 2703 |
. . . . . . . . . . 11
Scalar |
96 | | eqid 2622 |
. . . . . . . . . . . 12
Scalar Scalar |
97 | | eqid 2622 |
. . . . . . . . . . . 12
Scalar Scalar |
98 | 81, 96, 97, 5, 85, 10 | asclmul1 19339 |
. . . . . . . . . . 11
AssAlg
Scalar
algSc |
99 | 90, 95, 41, 98 | syl3anc 1326 |
. . . . . . . . . 10
algSc |
100 | 99 | fveq2d 6195 |
. . . . . . . . 9
algSc
|
101 | 24, 84 | ffvelrnd 6360 |
. . . . . . . . . . 11
algSc s |
102 | 24, 41 | ffvelrnd 6360 |
. . . . . . . . . . 11
s |
103 | 16, 17, 6, 20, 101, 102, 11, 86 | pwsmulrval 16151 |
. . . . . . . . . 10
algSc s algSc |
104 | 2, 3, 4, 81 | evl1sca 19698 |
. . . . . . . . . . . 12
algSc |
105 | 6, 9, 104 | syl2anc 693 |
. . . . . . . . . . 11
algSc |
106 | 2, 7, 4 | evl1var 19700 |
. . . . . . . . . . . 12
|
107 | 6, 106 | syl 17 |
. . . . . . . . . . 11
|
108 | 105, 107 | oveq12d 6668 |
. . . . . . . . . 10
algSc
|
109 | 103, 108 | eqtrd 2656 |
. . . . . . . . 9
algSc s |
110 | 88, 100, 109 | 3eqtr3d 2664 |
. . . . . . . 8
|
111 | 110 | fveq1d 6193 |
. . . . . . 7
|
112 | | fnconstg 6093 |
. . . . . . . . . 10
|
113 | 9, 112 | syl 17 |
. . . . . . . . 9
|
114 | | fnresi 6008 |
. . . . . . . . . 10
|
115 | 114 | a1i 11 |
. . . . . . . . 9
|
116 | | fnfvof 6911 |
. . . . . . . . 9
|
117 | 113, 115,
20, 80, 116 | syl22anc 1327 |
. . . . . . . 8
|
118 | | fvconst2g 6467 |
. . . . . . . . . . 11
|
119 | 9, 80, 118 | syl2anc 693 |
. . . . . . . . . 10
|
120 | | fvresi 6439 |
. . . . . . . . . . 11
|
121 | 80, 120 | syl 17 |
. . . . . . . . . 10
|
122 | 119, 121 | oveq12d 6668 |
. . . . . . . . 9
|
123 | 4, 11, 49 | ringrz 18588 |
. . . . . . . . . 10
|
124 | 39, 9, 123 | syl2anc 693 |
. . . . . . . . 9
|
125 | 122, 124 | eqtrd 2656 |
. . . . . . . 8
|
126 | 117, 125 | eqtrd 2656 |
. . . . . . 7
|
127 | 111, 126 | eqtrd 2656 |
. . . . . 6
|
128 | | fniniseg 6338 |
. . . . . . 7
|
129 | 28, 128 | syl 17 |
. . . . . 6
|
130 | 80, 127, 129 | mpbir2and 957 |
. . . . 5
|
131 | 130 | snssd 4340 |
. . . 4
|
132 | | hashsng 13159 |
. . . . . . 7
|
133 | 80, 132 | syl 17 |
. . . . . 6
|
134 | | ssdomg 8001 |
. . . . . . . . . 10
|
135 | 34, 131, 134 | mpsyl 68 |
. . . . . . . . 9
|
136 | | snfi 8038 |
. . . . . . . . . 10
|
137 | | hashdom 13168 |
. . . . . . . . . 10
|
138 | 136, 34, 137 | mp2an 708 |
. . . . . . . . 9
|
139 | 135, 138 | sylibr 224 |
. . . . . . . 8
|
140 | 133, 139 | eqbrtrrd 4677 |
. . . . . . 7
|
141 | | hashcl 13147 |
. . . . . . . . . 10
|
142 | 78, 141 | syl 17 |
. . . . . . . . 9
|
143 | 142 | nn0red 11352 |
. . . . . . . 8
|
144 | | 1re 10039 |
. . . . . . . 8
|
145 | | letri3 10123 |
. . . . . . . 8
|
146 | 143, 144,
145 | sylancl 694 |
. . . . . . 7
|
147 | 76, 140, 146 | mpbir2and 957 |
. . . . . 6
|
148 | 133, 147 | eqtr4d 2659 |
. . . . 5
|
149 | | hashen 13135 |
. . . . . 6
|
150 | 136, 78, 149 | sylancr 695 |
. . . . 5
|
151 | 148, 150 | mpbid 222 |
. . . 4
|
152 | | fisseneq 8171 |
. . . 4
|
153 | 78, 131, 151, 152 | syl3anc 1326 |
. . 3
|
154 | 31, 153 | eleqtrrd 2704 |
. 2
|
155 | | elsni 4194 |
. 2
|
156 | 154, 155 | syl 17 |
1
|