Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  plypf1 Structured version   Visualization version   Unicode version

Theorem plypf1 23245
 Description: Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015.) (Proof shortened by AV, 29-Sep-2019.)
Hypotheses
Ref Expression
plypf1.r flds
plypf1.p Poly1
plypf1.a
plypf1.e eval1fld
Assertion
Ref Expression
plypf1 SubRingfld Poly

Proof of Theorem plypf1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elply 23228 . . . . 5 Poly
21simprbi 471 . . . 4 Poly
3 eqid 2471 . . . . . . . . 9 fld s fld s
4 cnfldbas 19051 . . . . . . . . 9 fld
5 eqid 2471 . . . . . . . . 9 fld s fld s
6 cnex 9638 . . . . . . . . . 10
76a1i 11 . . . . . . . . 9 SubRingfld
8 fzfid 12224 . . . . . . . . 9 SubRingfld
9 cnring 19067 . . . . . . . . . 10 fld
10 ringcmn 17889 . . . . . . . . . 10 fld fld CMnd
119, 10mp1i 13 . . . . . . . . 9 SubRingfld fld CMnd
124subrgss 18087 . . . . . . . . . . . . 13 SubRingfld
1312ad2antrr 740 . . . . . . . . . . . 12 SubRingfld
14 elmapi 7511 . . . . . . . . . . . . . . 15
1514ad2antll 743 . . . . . . . . . . . . . 14 SubRingfld
16 subrgsubg 18092 . . . . . . . . . . . . . . . . . . 19 SubRingfld SubGrpfld
17 cnfld0 19069 . . . . . . . . . . . . . . . . . . . 20 fld
1817subg0cl 16903 . . . . . . . . . . . . . . . . . . 19 SubGrpfld
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18 SubRingfld
2019adantr 472 . . . . . . . . . . . . . . . . 17 SubRingfld
2120snssd 4108 . . . . . . . . . . . . . . . 16 SubRingfld
22 ssequn2 3598 . . . . . . . . . . . . . . . 16
2321, 22sylib 201 . . . . . . . . . . . . . . 15 SubRingfld
2423feq3d 5726 . . . . . . . . . . . . . 14 SubRingfld
2515, 24mpbid 215 . . . . . . . . . . . . 13 SubRingfld
26 elfznn0 11913 . . . . . . . . . . . . 13
27 ffvelrn 6035 . . . . . . . . . . . . 13
2825, 26, 27syl2an 485 . . . . . . . . . . . 12 SubRingfld
2913, 28sseldd 3419 . . . . . . . . . . 11 SubRingfld
3029adantrl 730 . . . . . . . . . 10 SubRingfld
31 simprl 772 . . . . . . . . . . 11 SubRingfld
3226ad2antll 743 . . . . . . . . . . 11 SubRingfld
33 expcl 12328 . . . . . . . . . . 11
3431, 32, 33syl2anc 673 . . . . . . . . . 10 SubRingfld
3530, 34mulcld 9681 . . . . . . . . 9 SubRingfld
36 eqid 2471 . . . . . . . . . 10
376mptex 6152 . . . . . . . . . . 11
3837a1i 11 . . . . . . . . . 10 SubRingfld
39 fvex 5889 . . . . . . . . . . 11 fld s
4039a1i 11 . . . . . . . . . 10 SubRingfld fld s
4136, 8, 38, 40fsuppmptdm 7912 . . . . . . . . 9 SubRingfld finSupp fld s
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 17689 . . . . . . . 8 SubRingfld fld s g fld g
43 fzfid 12224 . . . . . . . . . 10 SubRingfld
4435anassrs 660 . . . . . . . . . 10 SubRingfld
4543, 44gsumfsum 19111 . . . . . . . . 9 SubRingfld fld g
4645mpteq2dva 4482 . . . . . . . 8 SubRingfld fld g
4742, 46eqtrd 2505 . . . . . . 7 SubRingfld fld s g
483pwsring 17921 . . . . . . . . . 10 fld fld s
499, 6, 48mp2an 686 . . . . . . . . 9 fld s
50 ringcmn 17889 . . . . . . . . 9 fld s fld s CMnd
5149, 50mp1i 13 . . . . . . . 8 SubRingfld fld s CMnd
52 cncrng 19066 . . . . . . . . . . 11 fld
53 plypf1.e . . . . . . . . . . . 12 eval1fld
54 eqid 2471 . . . . . . . . . . . 12 Poly1fld Poly1fld
5553, 54, 3, 4evl1rhm 18997 . . . . . . . . . . 11 fld Poly1fld RingHom fld s
5652, 55ax-mp 5 . . . . . . . . . 10 Poly1fld RingHom fld s
57 plypf1.r . . . . . . . . . . . 12 flds
58 plypf1.p . . . . . . . . . . . 12 Poly1
59 plypf1.a . . . . . . . . . . . 12
6054, 57, 58, 59subrgply1 18903 . . . . . . . . . . 11 SubRingfld SubRingPoly1fld
6160adantr 472 . . . . . . . . . 10 SubRingfld SubRingPoly1fld
62 rhmima 18117 . . . . . . . . . 10 Poly1fld RingHom fld s SubRingPoly1fld SubRingfld s
6356, 61, 62sylancr 676 . . . . . . . . 9 SubRingfld SubRingfld s
64 subrgsubg 18092 . . . . . . . . 9 SubRingfld s SubGrpfld s
65 subgsubm 16917 . . . . . . . . 9 SubGrpfld s SubMndfld s
6663, 64, 653syl 18 . . . . . . . 8 SubRingfld SubMndfld s
67 eqid 2471 . . . . . . . . . . . 12 fld s fld s
689a1i 11 . . . . . . . . . . . 12 SubRingfld fld
696a1i 11 . . . . . . . . . . . 12 SubRingfld
70 fconst6g 5785 . . . . . . . . . . . . . 14
7129, 70syl 17 . . . . . . . . . . . . 13 SubRingfld
723, 4, 67pwselbasb 15464 . . . . . . . . . . . . . 14 fld fld s
739, 6, 72mp2an 686 . . . . . . . . . . . . 13 fld s
7471, 73sylibr 217 . . . . . . . . . . . 12 SubRingfld fld s
7534anass1rs 824 . . . . . . . . . . . . . 14 SubRingfld
76 eqid 2471 . . . . . . . . . . . . . 14
7775, 76fmptd 6061 . . . . . . . . . . . . 13 SubRingfld
783, 4, 67pwselbasb 15464 . . . . . . . . . . . . . 14 fld fld s
799, 6, 78mp2an 686 . . . . . . . . . . . . 13 fld s
8077, 79sylibr 217 . . . . . . . . . . . 12 SubRingfld fld s
81 cnfldmul 19053 . . . . . . . . . . . 12 fld
82 eqid 2471 . . . . . . . . . . . 12 fld s fld s
833, 67, 68, 69, 74, 80, 81, 82pwsmulrval 15467 . . . . . . . . . . 11 SubRingfld fld s
8429adantr 472 . . . . . . . . . . . 12 SubRingfld
85 fconstmpt 4883 . . . . . . . . . . . . 13
8685a1i 11 . . . . . . . . . . . 12 SubRingfld
87 eqidd 2472 . . . . . . . . . . . 12 SubRingfld
8869, 84, 75, 86, 87offval2 6567 . . . . . . . . . . 11 SubRingfld
8983, 88eqtrd 2505 . . . . . . . . . 10 SubRingfld fld s
9063adantr 472 . . . . . . . . . . 11 SubRingfld SubRingfld s
91 eqid 2471 . . . . . . . . . . . . . 14 algScPoly1fld algScPoly1fld
9253, 54, 4, 91evl1sca 18999 . . . . . . . . . . . . 13 fld algScPoly1fld
9352, 29, 92sylancr 676 . . . . . . . . . . . 12 SubRingfld algScPoly1fld
94 eqid 2471 . . . . . . . . . . . . . . . 16 Poly1fld Poly1fld
9594, 67rhmf 18032 . . . . . . . . . . . . . . 15 Poly1fld RingHom fld s Poly1fldfld s
9656, 95ax-mp 5 . . . . . . . . . . . . . 14 Poly1fldfld s
97 ffn 5739 . . . . . . . . . . . . . 14 Poly1fldfld s Poly1fld
9896, 97mp1i 13 . . . . . . . . . . . . 13 SubRingfld Poly1fld
9994subrgss 18087 . . . . . . . . . . . . . . 15 SubRingPoly1fld Poly1fld
10060, 99syl 17 . . . . . . . . . . . . . 14 SubRingfld Poly1fld
101100ad2antrr 740 . . . . . . . . . . . . 13 SubRingfld Poly1fld
102 simpll 768 . . . . . . . . . . . . . . 15 SubRingfld SubRingfld
10354, 91, 57, 58, 102, 59, 4, 29subrg1asclcl 18930 . . . . . . . . . . . . . 14 SubRingfld algScPoly1fld
10428, 103mpbird 240 . . . . . . . . . . . . 13 SubRingfld algScPoly1fld
105 fnfvima 6161 . . . . . . . . . . . . 13 Poly1fld Poly1fld algScPoly1fld algScPoly1fld
10698, 101, 104, 105syl3anc 1292 . . . . . . . . . . . 12 SubRingfld algScPoly1fld
10793, 106eqeltrrd 2550 . . . . . . . . . . 11 SubRingfld
10867subrgss 18087 . . . . . . . . . . . . . . . . 17 SubRingfld s fld s
10990, 108syl 17 . . . . . . . . . . . . . . . 16 SubRingfld fld s
11060ad2antrr 740 . . . . . . . . . . . . . . . . . . 19 SubRingfld SubRingPoly1fld
111 eqid 2471 . . . . . . . . . . . . . . . . . . . 20 mulGrpPoly1fld mulGrpPoly1fld
112111subrgsubm 18099 . . . . . . . . . . . . . . . . . . 19 SubRingPoly1fld SubMndmulGrpPoly1fld
113110, 112syl 17 . . . . . . . . . . . . . . . . . 18 SubRingfld SubMndmulGrpPoly1fld
11426adantl 473 . . . . . . . . . . . . . . . . . 18 SubRingfld
115 eqid 2471 . . . . . . . . . . . . . . . . . . 19 var1fld var1fld
116115, 102, 57, 58, 59subrgvr1cl 18932 . . . . . . . . . . . . . . . . . 18 SubRingfld var1fld
117 eqid 2471 . . . . . . . . . . . . . . . . . . 19 .gmulGrpPoly1fld .gmulGrpPoly1fld
118117submmulgcl 16870 . . . . . . . . . . . . . . . . . 18 SubMndmulGrpPoly1fld var1fld .gmulGrpPoly1fldvar1fld
119113, 114, 116, 118syl3anc 1292 . . . . . . . . . . . . . . . . 17 SubRingfld .gmulGrpPoly1fldvar1fld
120 fnfvima 6161 . . . . . . . . . . . . . . . . 17 Poly1fld Poly1fld .gmulGrpPoly1fldvar1fld .gmulGrpPoly1fldvar1fld
12198, 101, 119, 120syl3anc 1292 . . . . . . . . . . . . . . . 16 SubRingfld .gmulGrpPoly1fldvar1fld
122109, 121sseldd 3419 . . . . . . . . . . . . . . 15 SubRingfld .gmulGrpPoly1fldvar1fld fld s
1233, 4, 67, 68, 69, 122pwselbas 15465 . . . . . . . . . . . . . 14 SubRingfld .gmulGrpPoly1fldvar1fld
124123feqmptd 5932 . . . . . . . . . . . . 13 SubRingfld .gmulGrpPoly1fldvar1fld .gmulGrpPoly1fldvar1fld
12552a1i 11 . . . . . . . . . . . . . . . . 17 SubRingfld fld
126 simpr 468 . . . . . . . . . . . . . . . . 17 SubRingfld
12753, 115, 4, 54, 94, 125, 126evl1vard 19002 . . . . . . . . . . . . . . . . 17 SubRingfld var1fld Poly1fld var1fld
128 eqid 2471 . . . . . . . . . . . . . . . . 17 .gmulGrpfld .gmulGrpfld
129114adantr 472 . . . . . . . . . . . . . . . . 17 SubRingfld
13053, 54, 4, 94, 125, 126, 127, 117, 128, 129evl1expd 19010 . . . . . . . . . . . . . . . 16 SubRingfld .gmulGrpPoly1fldvar1fld Poly1fld .gmulGrpPoly1fldvar1fld .gmulGrpfld
131130simprd 470 . . . . . . . . . . . . . . 15 SubRingfld .gmulGrpPoly1fldvar1fld .gmulGrpfld
132 cnfldexp 19078 . . . . . . . . . . . . . . . 16 .gmulGrpfld
133126, 129, 132syl2anc 673 . . . . . . . . . . . . . . 15 SubRingfld .gmulGrpfld
134131, 133eqtrd 2505 . . . . . . . . . . . . . 14 SubRingfld .gmulGrpPoly1fldvar1fld
135134mpteq2dva 4482 . . . . . . . . . . . . 13 SubRingfld .gmulGrpPoly1fldvar1fld
136124, 135eqtrd 2505 . . . . . . . . . . . 12 SubRingfld .gmulGrpPoly1fldvar1fld
137136, 121eqeltrrd 2550 . . . . . . . . . . 11 SubRingfld
13882subrgmcl 18098 . . . . . . . . . . 11 SubRingfld s fld s
13990, 107, 137, 138syl3anc 1292 . . . . . . . . . 10 SubRingfld fld s
14089, 139eqeltrrd 2550 . . . . . . . . 9 SubRingfld
141140, 36fmptd 6061 . . . . . . . 8 SubRingfld
14236, 8, 140, 40fsuppmptdm 7912 . . . . . . . 8 SubRingfld finSupp fld s
1435, 51, 8, 66, 141, 142gsumsubmcl 17630 . . . . . . 7 SubRingfld fld s g
14447, 143eqeltrrd 2550 . . . . . 6 SubRingfld
145 eleq1 2537 . . . . . 6
146144, 145syl5ibrcom 230 . . . . 5 SubRingfld
147146rexlimdvva 2878 . . . 4 SubRingfld
1482, 147syl5 32 . . 3 SubRingfld Poly
149 ffun 5742 . . . . . 6 Poly1fldfld s
15096, 149ax-mp 5 . . . . 5
151 fvelima 5931 . . . . 5
152150, 151mpan 684 . . . 4
153100sselda 3418 . . . . . . . . . . 11 SubRingfld Poly1fld
154 eqid 2471 . . . . . . . . . . . 12 Poly1fld Poly1fld
155 eqid 2471 . . . . . . . . . . . 12 coe1 coe1
15654, 115, 94, 154, 111, 117, 155ply1coe 18966 . . . . . . . . . . 11 fld Poly1fld Poly1fld g coe1Poly1fld.gmulGrpPoly1fldvar1fld
1579, 153, 156sylancr 676 . . . . . . . . . 10 SubRingfld Poly1fld g coe1Poly1fld.gmulGrpPoly1fldvar1fld
158157fveq2d 5883 . . . . . . . . 9 SubRingfld Poly1fld g coe1Poly1fld.gmulGrpPoly1fldvar1fld
159 eqid 2471 . . . . . . . . . 10 Poly1fld Poly1fld
16054ply1ring 18918 . . . . . . . . . . . 12 fld Poly1fld
1619, 160ax-mp 5 . . . . . . . . . . 11 Poly1fld
162 ringcmn 17889 . . . . . . . . . . 11 Poly1fld Poly1fld CMnd
163161, 162mp1i 13 . . . . . . . . . 10 SubRingfld Poly1fld CMnd
164 ringmnd 17867 . . . . . . . . . . 11 fld s fld s
16549, 164mp1i 13 . . . . . . . . . 10 SubRingfld fld s
166 nn0ex 10899 . . . . . . . . . . 11
167166a1i 11 . . . . . . . . . 10 SubRingfld
168 rhmghm 18031 . . . . . . . . . . . 12 Poly1fld RingHom fld s Poly1fld fld s
16956, 168ax-mp 5 . . . . . . . . . . 11 Poly1fld fld s
170 ghmmhm 16971 . . . . . . . . . . 11 Poly1fld fld s Poly1fld MndHom fld s
171169, 170mp1i 13 . . . . . . . . . 10 SubRingfld Poly1fld MndHom fld s
17254ply1lmod 18922 . . . . . . . . . . . . 13 fld Poly1fld
1739, 172mp1i 13 . . . . . . . . . . . 12 SubRingfld Poly1fld
17412ad2antrr 740 . . . . . . . . . . . . 13 SubRingfld
175 eqid 2471 . . . . . . . . . . . . . . . . 17
176155, 59, 58, 175coe1f 18881 . . . . . . . . . . . . . . . 16 coe1
17757subrgbas 18095 . . . . . . . . . . . . . . . . 17 SubRingfld
178177feq3d 5726 . . . . . . . . . . . . . . . 16 SubRingfld coe1 coe1
179176, 178syl5ibr 229 . . . . . . . . . . . . . . 15 SubRingfld coe1
180179imp 436 . . . . . . . . . . . . . 14 SubRingfld coe1
181180ffvelrnda 6037 . . . . . . . . . . . . 13 SubRingfld coe1
182174, 181sseldd 3419 . . . . . . . . . . . 12 SubRingfld coe1
183111ringmgp 17864 . . . . . . . . . . . . . 14 Poly1fld mulGrpPoly1fld
184161, 183mp1i 13 . . . . . . . . . . . . 13 SubRingfld mulGrpPoly1fld
185 simpr 468 . . . . . . . . . . . . 13 SubRingfld
186115, 54, 94vr1cl 18887 . . . . . . . . . . . . . 14 fld var1fld Poly1fld
1879, 186mp1i 13 . . . . . . . . . . . . 13 SubRingfld var1fld Poly1fld
188111, 94mgpbas 17807 . . . . . . . . . . . . . 14 Poly1fld mulGrpPoly1fld
189188, 117mulgnn0cl 16852 . . . . . . . . . . . . 13 mulGrpPoly1fld var1fld Poly1fld .gmulGrpPoly1fldvar1fld Poly1fld
190184, 185, 187, 189syl3anc 1292 . . . . . . . . . . . 12 SubRingfld .gmulGrpPoly1fldvar1fld Poly1fld
19154ply1sca 18923 . . . . . . . . . . . . . 14 fld fld ScalarPoly1fld
1929, 191ax-mp 5 . . . . . . . . . . . . 13 fld ScalarPoly1fld
19394, 192, 154, 4lmodvscl 18186 . . . . . . . . . . . 12 Poly1fld coe1 .gmulGrpPoly1fldvar1fld Poly1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld
194173, 182, 190, 193syl3anc 1292 . . . . . . . . . . 11 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld
195 eqid 2471 . . . . . . . . . . 11 coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld
196194, 195fmptd 6061 . . . . . . . . . 10 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fldPoly1fld
197166mptex 6152 . . . . . . . . . . . . 13 coe1Poly1fld.gmulGrpPoly1fldvar1fld
198 funmpt 5625 . . . . . . . . . . . . 13 coe1Poly1fld.gmulGrpPoly1fldvar1fld
199 fvex 5889 . . . . . . . . . . . . 13 Poly1fld
200197, 198, 1993pm3.2i 1208 . . . . . . . . . . . 12 coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld
201200a1i 11 . . . . . . . . . . 11 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld
202155, 94, 54, 17coe1sfi 18883 . . . . . . . . . . . . 13 Poly1fld coe1 finSupp
203153, 202syl 17 . . . . . . . . . . . 12 SubRingfld coe1 finSupp
204203fsuppimpd 7908 . . . . . . . . . . 11 SubRingfld coe1 supp
205180feqmptd 5932 . . . . . . . . . . . . . 14 SubRingfld coe1 coe1
206205oveq1d 6323 . . . . . . . . . . . . 13 SubRingfld coe1 supp coe1 supp
207 eqimss2 3471 . . . . . . . . . . . . 13 coe1 supp coe1 supp coe1 supp coe1 supp
208206, 207syl 17 . . . . . . . . . . . 12 SubRingfld coe1 supp coe1 supp
2099, 172mp1i 13 . . . . . . . . . . . . 13 SubRingfld Poly1fld
21094, 192, 154, 17, 159lmod0vs 18202 . . . . . . . . . . . . 13 Poly1fld Poly1fld Poly1fld Poly1fld
211209, 210sylan 479 . . . . . . . . . . . 12 SubRingfld Poly1fld Poly1fld Poly1fld
212 c0ex 9655 . . . . . . . . . . . . 13
213212a1i 11 . . . . . . . . . . . 12 SubRingfld
214208, 211, 181, 190, 213suppssov1 6966 . . . . . . . . . . 11 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld supp Poly1fld coe1 supp
215 suppssfifsupp 7916 . . . . . . . . . . 11 coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld coe1 supp coe1Poly1fld.gmulGrpPoly1fldvar1fld supp Poly1fld coe1 supp coe1Poly1fld.gmulGrpPoly1fldvar1fld finSupp Poly1fld
216201, 204, 214, 215syl12anc 1290 . . . . . . . . . 10 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld finSupp Poly1fld
21794, 159, 163, 165, 167, 171, 196, 216gsummhm 17649 . . . . . . . . 9 SubRingfld fld s g coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld g coe1Poly1fld.gmulGrpPoly1fldvar1fld
218 eqidd 2472 . . . . . . . . . . . 12 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld
21996a1i 11 . . . . . . . . . . . . 13 SubRingfld Poly1fldfld s
220219feqmptd 5932 . . . . . . . . . . . 12 SubRingfld Poly1fld
221 fveq2 5879 . . . . . . . . . . . 12 coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld
222194, 218, 220, 221fmptco 6072 . . . . . . . . . . 11 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld
2239a1i 11 . . . . . . . . . . . . . . 15 SubRingfld fld
2246a1i 11 . . . . . . . . . . . . . . 15 SubRingfld
22596ffvelrni 6036 . . . . . . . . . . . . . . . 16 coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld fld s
226194, 225syl 17 . . . . . . . . . . . . . . 15 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld fld s
2273, 4, 67, 223, 224, 226pwselbas 15465 . . . . . . . . . . . . . 14 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld
228227feqmptd 5932 . . . . . . . . . . . . 13 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld
22952a1i 11 . . . . . . . . . . . . . . . 16 SubRingfld fld
230 simpr 468 . . . . . . . . . . . . . . . 16 SubRingfld
23153, 115, 4, 54, 94, 229, 230evl1vard 19002 . . . . . . . . . . . . . . . . . 18 SubRingfld var1fld Poly1fld var1fld
232185adantr 472 . . . . . . . . . . . . . . . . . 18 SubRingfld
23353, 54, 4, 94, 229, 230, 231, 117, 128, 232evl1expd 19010 . . . . . . . . . . . . . . . . 17 SubRingfld .gmulGrpPoly1fldvar1fld Poly1fld .gmulGrpPoly1fldvar1fld .gmulGrpfld
234230, 232, 132syl2anc 673 . . . . . . . . . . . . . . . . . . 19 SubRingfld .gmulGrpfld
235234eqeq2d 2481 . . . . . . . . . . . . . . . . . 18 SubRingfld .gmulGrpPoly1fldvar1fld .gmulGrpfld .gmulGrpPoly1fldvar1fld
236235anbi2d 718 . . . . . . . . . . . . . . . . 17 SubRingfld .gmulGrpPoly1fldvar1fld Poly1fld .gmulGrpPoly1fldvar1fld .gmulGrpfld .gmulGrpPoly1fldvar1fld Poly1fld .gmulGrpPoly1fldvar1fld
237233, 236mpbid 215 . . . . . . . . . . . . . . . 16 SubRingfld .gmulGrpPoly1fldvar1fld Poly1fld .gmulGrpPoly1fldvar1fld
238182adantr 472 . . . . . . . . . . . . . . . 16 SubRingfld coe1
23953, 54, 4, 94, 229, 230, 237, 238, 154, 81evl1vsd 19009 . . . . . . . . . . . . . . 15 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld Poly1fld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1
240239simprd 470 . . . . . . . . . . . . . 14 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1
241240mpteq2dva 4482 . . . . . . . . . . . . 13 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1
242228, 241eqtrd 2505 . . . . . . . . . . . 12 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1
243242mpteq2dva 4482 . . . . . . . . . . 11 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1
244222, 243eqtrd 2505 . . . . . . . . . 10 SubRingfld coe1Poly1fld.gmulGrpPoly1fldvar1fld coe1
245244oveq2d 6324 . . . . . . . . 9 SubRingfld fld s g coe1Poly1fld.gmulGrpPoly1fldvar1fld fld s g coe1
246158, 217, 2453eqtr2d 2511 . . . . . . . 8 SubRingfld fld s g coe1
2476a1i 11 . . . . . . . . 9 SubRingfld
2489, 10mp1i 13 . . . . . . . . 9 SubRingfld fld CMnd
249182adantlr 729 . . . . . . . . . . 11 SubRingfld coe1
25033adantll 728 . . . . . . . . . . 11 SubRingfld
251249, 250mulcld 9681 . . . . . . . . . 10 SubRingfld coe1
252251anasss 659 . . . . . . . . 9 SubRingfld coe1
253166mptex 6152 . . . . . . . . . . . 12 coe1
254 funmpt 5625 . . . . . . . . . . . 12 coe1
255253, 254, 393pm3.2i 1208 . . . . . . . . . . 11 coe1 coe1 fld s
256255a1i 11 . . . . . . . . . 10 SubRingfld coe1 coe1 fld s
257 fzfid 12224 . . . . . . . . . 10 SubRingfld deg1 fld deg1 fld
258 eldifn 3545 . . . . . . . . . . . . . . . . . 18 deg1 fld deg1 fld deg1 fld deg1 fld
259258adantl 473 . . . . . . . . . . . . . . . . 17 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld
260153ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . 22 SubRingfld deg1 fld deg1 fld Poly1fld
261 eldifi 3544 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 fld deg1 fld
262261adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 SubRingfld deg1 fld deg1 fld
263 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . 24 deg1 fld deg1 fld
264263, 54, 94, 17, 155deg1ge 23126 . . . . . . . . . . . . . . . . . . . . . . 23 Poly1fld coe1 deg1 fld
2652643expia 1233 . . . . . . . . . . . . . . . . . . . . . 22 Poly1fld coe1 deg1 fld
266260, 262, 265syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21 SubRingfld deg1 fld deg1 fld coe1 deg1 fld
267 0xr 9705 . . . . . . . . . . . . . . . . . . . . . . 23
268263, 54, 94deg1xrcl 23110 . . . . . . . . . . . . . . . . . . . . . . . . 25 Poly1fld deg1 fld
269153, 268syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 SubRingfld deg1 fld
270269ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . 23 SubRingfld deg1 fld deg1 fld deg1 fld
271 xrmax2 11494 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 fld deg1 fld deg1 fld deg1 fld
272267, 270, 271sylancr 676 . . . . . . . . . . . . . . . . . . . . . 22 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld
273262nn0red 10950 . . . . . . . . . . . . . . . . . . . . . . . 24 SubRingfld deg1 fld deg1 fld
274273rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . 23 SubRingfld deg1 fld deg1 fld
275 ifcl 3914 . . . . . . . . . . . . . . . . . . . . . . . 24 deg1 fld deg1 fld deg1 fld
276270, 267, 275sylancl 675 . . . . . . . . . . . . . . . . . . . . . . 23 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld
277 xrletr 11478 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld
278274, 270, 276, 277syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . 22 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld
279272, 278mpan2d 688 . . . . . . . . . . . . . . . . . . . . 21 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld
280266, 279syld 44 . . . . . . . . . . . . . . . . . . . 20 SubRingfld deg1 fld deg1 fld coe1 deg1 fld deg1 fld
281280, 262jctild 552 . . . . . . . . . . . . . . . . . . 19 SubRingfld deg1 fld deg1 fld coe1 deg1 fld deg1 fld
282263, 54, 94deg1cl 23111 . . . . . . . . . . . . . . . . . . . . . . . 24 Poly1fld deg1 fld
283153, 282syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 SubRingfld deg1 fld
284 elun 3565 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 fld deg1 fld deg1 fld
285283, 284sylib 201 . . . . . . . . . . . . . . . . . . . . . 22 SubRingfld deg1 fld deg1 fld
286 nn0ge0 10919 . . . . . . . . . . . . . . . . . . . . . . . . 25 deg1 fld deg1 fld
287286iftrued 3880 . . . . . . . . . . . . . . . . . . . . . . . 24 deg1 fld deg1 fld deg1 fld deg1 fld
288 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 deg1 fld deg1 fld
289287, 288eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 fld deg1 fld deg1 fld
290 mnflt0 11450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
291 mnfxr 11437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
292 xrltnle 9719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
293291, 267, 292mp2an 686 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
294290, 293mpbi 213 . . . . . . . . . . . . . . . . . . . . . . . . . 26
295 elsni 3985 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 deg1 fld deg1 fld
296295breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . . . . 26 deg1 fld deg1 fld
297294, 296mtbiri 310 . . . . . . . . . . . . . . . . . . . . . . . . 25 deg1 fld deg1 fld
298297iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . 24 deg1 fld deg1 fld deg1 fld
299 0nn0 10908 . . . . . . . . . . . . . . . . . . . . . . . 24
300298, 299syl6eqel 2557 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 fld deg1 fld deg1 fld
301289, 300jaoi 386 . . . . . . . . . . . . . . . . . . . . . 22 deg1 fld deg1 fld deg1 fld deg1 fld
302285, 301syl 17 . . . . . . . . . . . . . . . . . . . . 21 SubRingfld deg1 fld deg1 fld
303302ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld
304 fznn0 11912 . . . . . . . . . . . . . . . . . . . 20 deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld
305303, 304syl 17 . . . . . . . . . . . . . . . . . . 19 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld deg1 fld
306281, 305sylibrd 242 . . . . . . . . . . . . . . . . . 18 SubRingfld deg1 fld deg1 fld coe1 deg1 fld deg1 fld
307306necon1bd 2661 . . . . . . . . . . . . . . . . 17 SubRingfld deg1 fld deg1 fld deg1 fld deg1 fld coe1
308259, 307mpd 15 . . . . . . . . . . . . . . . 16 SubRingfld deg1 fld deg1 fld coe1
309308oveq1d 6323 . . . . . . . . . . . . . . 15 SubRingfld deg1 fld deg1 fld coe1
310261, 250sylan2 482 . . . . . . . . . . . . . . . 16 SubRingfld deg1 fld deg1 fld
311310mul02d 9849 . . . . . . . . . . . . . . 15 SubRingfld deg1 fld deg1 fld
312309, 311eqtrd 2505 . . . . . . . . . . . . . 14 SubRingfld deg1 fld deg1 fld coe1
313312an32s 821 . . . . . . . . . . . . 13 SubRingfld deg1 fld deg1 fld coe1
314313mpteq2dva 4482 . . . . . . . . . . . 12 SubRingfld deg1 fld deg1 fld coe1
315 fconstmpt 4883 . . . . . . . . . . . . 13
316 ringmnd 17867 . . . . . . . . . . . . . . 15 fld fld
3179, 316ax-mp 5 . . . . . . . . . . . . . 14 fld
3183, 17pws0g 16650 . . . . . . . . . . . . . 14 fld fld s
319317, 6, 318mp2an 686 . . . . . . . . . . . . 13 fld s
320315, 319eqtr3i 2495 . . . . . . . . . . . 12 fld s
321314, 320syl6eq 2521 . . . . . . . . . . 11 SubRingfld deg1 fld deg1 fld coe1 fld s
322321, 167suppss2 6968 . . . . . . . . . 10 SubRingfld coe1 supp fld s deg1 fld deg1 fld
323 suppssfifsupp 7916 . . . . . . . . . 10 coe1 coe1 fld s deg1 fld deg1 fld coe1 supp fld s deg1 fld deg1 fld coe1 finSupp fld s
324256, 257, 322, 323syl12anc 1290 . . . . . . . . 9 SubRingfld coe1 finSupp fld s
3253, 4, 5, 247, 167, 248, 252, 324pwsgsum 17689 . . . . . . . 8 SubRingfld fld s g coe1 fld g coe1
326 elfznn0 11913 . . . . . . . . . . . . 13 deg1 fld deg1 fld
327326ssriv 3422 . . . . . . . . . . . 12 deg1 fld deg1 fld
328 resmpt 5160 . . . . . . . . . . . 12 deg1 fld deg1 fld coe1 deg1 fld deg1 fld deg1 fld deg1 fld coe1
329327, 328ax-mp 5 . . . . . . . . . . 11 coe1 deg1 fld deg1 fld deg1 fld deg1 fld coe1
330329oveq2i 6319 . . . . . . . . . 10 fld g coe1 deg1 fld deg1 fld fld g deg1 fld deg1 fld coe1
3319, 10mp1i 13 . . . . . . . . . . 11 SubRingfld fld CMnd
332166a1i 11 . . . . . . . . . . 11