add a few more polynomial theorems to iset.mm (#5021)

* Add plyco to iset.mm

Stated as in set.mm.  The proof, although it is much rearranged, is
based on the set.mm proof.  The "degree" (really an upper bound
for the degree) and coefficients come from elply2 rather than from
deg and coeff .

Parts of the proof are broken out into lemma plycolemc .

* Add plycn to mmil.html

* Remove unneeded hypotheses

This is for plycj and coecj in set.mm.  Because N is not mentioned
in other hypotheses or the conclusion, there is no need for
the N = ( deg ` F ) hypothesis and the proof can just use ( deg ` F )
where it had used N .

The changes to plycjlem are just cosmetic (whitespace etc).

* Add plycj to iset.mm

Stated as in set.mm.  The proof is generally similar but the details are
different because it uses elply in place of deg and coeff .

Includes lemma plycjlemc which is similar to plycjlem from set.mm but
which specifies (an upper bound for a) degree and coefficients
explicitly rather than via deg and coeff .

Add coecj to mmil.html

* Add plyrecj to iset.mm

Stated as in set.mm.  The proof is based on the set.mm proof although it
is changed in many places, especially to handle coefficients via elply
rather than the coeff syntax.

Author: jkingdon

changes-set.txt

@@ -92,6 +92,8 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+23-Sep-25 coecj     [same]      Removed unneeded hypothesis
+23-Sep-25 plycj     [same]      Removed unneeded hypothesis
 23-Sep-25 elfzolem1 [same]      moved from GS's mathbox to main set.mm
 17-Sep-25 psdmul    [same]      Removed unneeded hypothesis
 17-Sep-25 psdvsca   [same]      Removed unneeded hypothesis

discouraged

@@ -12362,6 +12362,7 @@
 "plusgndx" is used by "topgrpstr".
 "plusgndx" is used by "tsetndxnplusgndx".
 "plusgndx" is used by "vscandxnplusgndx".
+"plycjOLD" is used by "coecjOLD".
 "pm2.43cbi" is used by "ee233".
 "pm2.43cbi" is used by "ee33VD".
 "pmap1N" is used by "pmapglb2N".
@@ -15925,6 +15926,7 @@ New usage of "cnvoprabOLD" is discouraged (0 uses).
 New usage of "cnvsymOLD" is discouraged (0 uses).
 New usage of "cnvsymOLDOLD" is discouraged (0 uses).
 New usage of "cnvunop" is discouraged (2 uses).
+New usage of "coecjOLD" is discouraged (0 uses).
 New usage of "com3rgbi" is discouraged (1 uses).
 New usage of "con3ALT" is discouraged (0 uses).
 New usage of "con3ALT2" is discouraged (0 uses).
@@ -18781,6 +18783,7 @@ New usage of "ply1basOLD" is discouraged (0 uses).
 New usage of "ply1idvr1OLD" is discouraged (0 uses).
 New usage of "ply1scl0OLD" is discouraged (0 uses).
 New usage of "ply1scl1OLD" is discouraged (0 uses).
+New usage of "plycjOLD" is discouraged (1 uses).
 New usage of "plycnOLD" is discouraged (0 uses).
 New usage of "pm10.252" is discouraged (0 uses).
 New usage of "pm11.07" is discouraged (0 uses).
@@ -20336,6 +20339,7 @@ Proof modification of "cnvopabOLD" is discouraged (77 steps).
 Proof modification of "cnvoprabOLD" is discouraged (262 steps).
 Proof modification of "cnvsymOLD" is discouraged (69 steps).
 Proof modification of "cnvsymOLDOLD" is discouraged (88 steps).
+Proof modification of "coecjOLD" is discouraged (263 steps).
 Proof modification of "com3rgbi" is discouraged (35 steps).
 Proof modification of "con3ALT" is discouraged (54 steps).
 Proof modification of "con3ALT2" is discouraged (14 steps).
@@ -21312,6 +21316,7 @@ Proof modification of "ply1basOLD" is discouraged (58 steps).
 Proof modification of "ply1idvr1OLD" is discouraged (151 steps).
 Proof modification of "ply1scl0OLD" is discouraged (137 steps).
 Proof modification of "ply1scl1OLD" is discouraged (132 steps).
+Proof modification of "plycjOLD" is discouraged (283 steps).
 Proof modification of "plycnOLD" is discouraged (172 steps).
 Proof modification of "pm13.181OLD" is discouraged (20 steps).
 Proof modification of "pm2.21ddALT" is discouraged (10 steps).

iset.mm

@@ -179136,6 +179136,193 @@ theorem as stated here (although versions with additional conditions,
       CISUJUDUEUF $.
   $}
 
+  ${
+    plyco.1 $e |- ( ph -> F e. ( Poly ` S ) ) $.
+    plyco.2 $e |- ( ph -> G e. ( Poly ` S ) ) $.
+    plyco.3 $e |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S ) $.
+    plyco.4 $e |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S ) $.
+    ${
+      plycolemc.n $e |- ( ph -> N e. NN0 ) $.
+      plycolemc.a $e |- ( ph -> A : NN0 --> ( S u. { 0 } ) ) $.
+      plycolemc.z $e |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) $.
+      plycolemc.f $e |- ( ph -> F = ( x e. CC |-> sum_ k e. ( 0 ... N )
+        ( ( A ` k ) x. ( x ^ k ) ) ) ) $.
+      $d G k z $.  $d A k $.  $d N k $.  $d A d k x y w z $.
+      $d G d k x y w z $.  $d N k w z $.  $d S d x y w $.  $d ph k x y z d w $.
+      $( Lemma for ~ plyco .  The result expressed as a sum, with a degree and
+         coefficients for ` F ` specified as hypotheses.  (Contributed by Jim
+         Kingdon, 20-Sep-2025.) $)
+      plycolemc $p |- ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N )
+          ( ( A ` k ) x. ( ( G ` z ) ^ k ) ) ) e. ( Poly ` S ) ) $=
+        ( wcel cc vw vd cn0 cc0 cfz co cv cfv cexp cmul cmpt cply wi caddc wceq
+        csu c1 oveq2 sumeq1d mpteq2dv eleq1d imbi2d csn cxp wa cz 0z ffvelcdmda
+        wf plyf syl exp0d oveq2d cun wss plybss 0cnd snssd unssd 0nn0 ffvelcdmd
+        a1i sseldd adantr mulridd eqtrd eqeltrd fveq2 oveq12d sylancr mpteq2dva
+        fconstmpt eqtr4di plyconst syl2anc plyun0 eleqtrdi cof simprr peano2nn0
+        fsum1 ffvelcdm syl2an cn nn0p1nn feqmptd eqtr4d adantlr plymul expr cvv
+        exp1d cnex nnnn0 ad2antlr expcld eqidd offval2 expp1d sylibd expcom a2d
+        nnind impcom adantrr plyadd 0zd simplr nn0zd fzfigd eleqtrrdi ad3antrrr
+        elfznn0 adantl ad4ant13 mulcld fsumcl ad2antrr cuz nn0uz fsump1 nn0ind
+        mpcom ) JUCSADTUDJUEUFZGUGZEUHZDUGZIUHZUUEUIUFZUJUFZGUPZUKZFULUHZSZOADT
+        UDUAUGZUEUFZUUJGUPZUKZUUMSZUMADTUDUDUEUFZUUJGUPZUKZUUMSZUMADTUDUBUGZUEU
+        FZUUJGUPZUKZUUMSZUMADTUDUVDUQUNUFZUEUFZUUJGUPZUKZUUMSZUMAUUNUMUAUBJUUOU
+        DUOZUUSUVCAUVNUURUVBUUMUVNDTUUQUVAUVNUUPUUTUUJGUUOUDUDUEURUSUTVAVBUUOUV
+        DUOZUUSUVHAUVOUURUVGUUMUVODTUUQUVFUVOUUPUVEUUJGUUOUVDUDUEURUSUTVAVBUUOU
+        VIUOZUUSUVMAUVPUURUVLUUMUVPDTUUQUVKUVPUUPUVJUUJGUUOUVIUDUEURUSUTVAVBUUO
+        JUOZUUSUUNAUVQUURUULUUMUVQDTUUQUUKUVQUUPUUDUUJGUUOJUDUEURUSUTVAVBAUVBTU
+        DEUHZVCVDZUUMAUVBDTUVRUKUVSADTUVAUVRAUUGTSZVEZUVAUVRUUHUDUIUFZUJUFZUVRU
+        WAUDVFSUWCTSUVAUWCUOVGUWAUWCUVRTUWAUWCUVRUQUJUFUVRUWAUWBUQUVRUJUWAUUHAT
+        TUUGIAIUUMSZTTIVIZLFIVJVKZVHZVLVMUWAUVRAUVRTSUVTAFUDVCZVNZTUVRAFUWHTAHU
+        UMSFTVOKFHVPVKAUDTAVQVRVSZAUCUWIUDEPUDUCSAVTWBWAZWCWDZWEWFZUWLWGUUJUWCG
+        UDUUEUDUOUUFUVRUUIUWBUJUUEUDEWHUUEUDUUHUIURWIXAWJUWMWFWKDTUVRWLWMAUVSUW
+        IULUHZUUMAUWITVOZUVRUWISUVSUWNSUWJUWKUVRUWIWNWOFWPZWQWGUVDUCSZAUVHUVMAU
+        WQUVHUVMUMAUWQVEZUVHUVGTUVIEUHZVCVDZDTUUHUVIUIUFZUKZUJWRZUFZUNWRUFZUUMS
+        ZUVMAUWQUVHUXFAUWQUVHVEZVEBCFUVGUXDAUWQUVHWSAUWQUXDUUMSUVHUWRBCFUWTUXBU
+        WRUWTUWNUUMUWRUWOUWSUWISZUWTUWNSAUWOUWQUWJWDAUCUWIEVIZUVIUCSZUXHUWQPUVD
+        WTZUCUWIUVIEXBXCZUWSUWIWNWOUWPWQUWQAUXBUUMSZUWQUVIXDSAUXMUMZUVDXEADTUUH
+        UUOUIUFZUKZUUMSZUMADTUUHUQUIUFZUKZUUMSZUMADTUUHUVDUIUFZUKZUUMSZUMUXNUXN
+        UAUBUVIUUOUQUOZUXQUXTAUYDUXPUXSUUMUYDDTUXOUXRUUOUQUUHUIURUTVAVBUVOUXQUY
+        CAUVOUXPUYBUUMUVODTUXOUYAUUOUVDUUHUIURUTVAVBUVPUXQUXMAUVPUXPUXBUUMUVPDT
+        UXOUXAUUOUVIUUHUIURUTVAVBZUYEAUXSIUUMAUXSDTUUHUKZIADTUXRUUHUWAUUHUWGXLW
+        KADTTIUWFXFZXGLWGUVDXDSZAUYCUXMAUYHUYCUXMUMAUYHVEZUYCUYBIUXCUFZUUMSZUXM
+        AUYHUYCUYKAUYHUYCVEZVEBCFUYBIAUYHUYCWSAUWDUYLLWDABUGZFSCUGZFSVEZUYMUYNU
+        NUFFSZUYLMXHAUYOUYMUYNUJUFFSZUYLNXHXIXJUYIUYJUXBUUMUYIUYJDTUYAUUHUJUFZU
+        KUXBUYIDTUYAUUHUJUYBIXKTTTXKSZUYIXMWBUYIUVTVEZUUHUVDAUVTUUHTSZUYHUWGXHZ
+        UYHUWQAUVTUVDXNXOZXPUYITTUUGIAUWEUYHUWFWDVHUYIUYBXQAIUYFUOUYHUYGWDXRUYI
+        DTUXAUYRUYTUUHUVDVUBVUCXSWKXGVAXTYAYBYCVKYDAUYOUYPUWQMXHAUYOUYQUWQNXHXI
+        YEAUYOUYPUXGMXHYFXJUWRUXEUVLUUMUWRUXEDTUVFUWSUXAUJUFZUNUFZUKUVLUWRDTUVF
+        VUDUNUVGUXDXKTTUYSUWRXMWBZUWRUVTVEZUVEUUJGVUGUDUVDVUGYGVUGUVDAUWQUVTYHZ
+        YIYJVUGUUEUVESZVEZUUFUUIVUJUWITUUFAUWOUWQUVTVUIAHUWNSUWOAHUUMUWNKUWPYKU
+        WIHVPVKZYLVUJUCUWIUUEEAUXIUWQUVTVUIPYLVUIUUEUCSZVUGUUEUVDYMYNZWAWCVUJUU
+        HUUEAUVTVUAUWQVUIUWGYOVUMXPYPYQVUGUWSUXAVUGUWITUWSAUWOUWQUVTVUKYRZUWRUX
+        HUVTUXLWDZWCVUGUUHUVIAUVTVUAUWQUWGXHZUWQUXJAUVTUXKXOXPZYPUWRUVGXQUWRDTU
+        WSUXAUJUWTUXBXKUWITVUFVUOVUQUWTDTUWSUKUOUWRDTUWSWLWBUWRUXBXQXRXRUWRDTUV
+        KVUEVUGUUJVUDGUDUVDVUGUVDUCUDYSUHVUHYTWQVUGUUEUVJSZVEZUUFUUIVUSUWITUUFV
+        UGUWOVURVUNWDVUSUCUWIUUEEAUXIUWQUVTVURPYLVURVULVUGUUEUVIYMYNZWAWCVUSUUH
+        UUEVUGVUAVURVUPWDVUTXPYPUUEUVIUOUUFUWSUUIUXAUJUUEUVIEWHUUEUVIUUHUIURWIU
+        UAWKXGVAXTYAYBUUBUUC $.
+    $}
+
+    $d F a k n x y z $.  $d G a k n x y z $.  $d d k x y z ph $.
+    $d a k n x y z S $.  $d a k n ph x y z w j $.
+    $( The composition of two polynomials is a polynomial.  (Contributed by
+       Mario Carneiro, 23-Jul-2014.)  (Revised by Mario Carneiro,
+       23-Aug-2014.) $)
+    plyco $p |- ( ph -> ( F o. G ) e. ( Poly ` S ) ) $=
+      ( vk cv co wceq cc cexp cmul wa wcel cvv va vn vz vw vj c1 caddc cuz cima
+      cfv cc0 csn cfz csu cmpt cun cn0 cmap wrex ccom cply wss elply2 simprd wf
+      sylib plyf syl ffvelcdmda ad4ant14 ad2antrr simprr oveq1 oveq2d sumeq2sdv
+      feqmptd fmptco cbvmptv fveq2 oveq2 oveq12d cbvsumv mpteq2i eqeq2i simplrl
+      eqtri anbi2i simplrr wb simpld cnex ssexg sylancl c0ex unexg nn0ex elmapg
+      snex mpbid sylbir simprl plycolemc sylbi eqeltrd ex rexlimdvva mpd ) AUAL
+      ZUBLZUFUGMUHUJUIUKULZNZEBOUKXIUMMZKLZXHUJZBLZXMPMZQMZKUNZUOZNZRZUADXJUPZU
+      QURMZUSUBUQUSZEFUTZDVAUJZSZADOVBZYDAEYFSZYHYDRGBDKUBEUAVCVFZVDAYAYGUBUAUQ
+      YCAXIUQSZXHYCSZRZRZYAYGYNYARZYEUCOXLXNUCLZFUJZXMPMZQMZKUNZUOZYFYOUCBOOYQX
+      RYTFEAYPOSYQOSYMYAAOOYPFAFYFSZOOFVEHDFVGVHZVIVJAFUCOYQUONYMYAAUCOOFUUCVPV
+      KYNXKXTVLZXOYQNZXLXQYSKUUEXPYRXNQXOYQXMPVMVNVOVQYOYNXKEUDOXLUELZXHUJZUDLZ
+      UUFPMZQMZUEUNZUOZNZRZRZUUAYFSYAUUNYNXTUUMXKXSUULEXSUDOXLXNUUHXMPMZQMZKUNZ
+      UOUULBUDOXRUURXOUUHNZXLXQUUQKUUSXPUUPXNQXOUUHXMPVMVNVOVRUDOUURUUKXLUUQUUJ
+      KUEXMUUFNXNUUGUUPUUIQXMUUFXHVSXMUUFUUHPVTWAWBWCWFWDWGWGZUUOBCUCXHDKEFXIAY
+      IYMUUNGVKAUUBYMUUNHVKAXODSCLZDSRZXOUVAUGMDSYMUUNIVJAUVBXOUVAQMDSYMUUNJVJA
+      YKYLUUNWEUUOYOUQYBXHVEZUUTYOYLUVCAYKYLYAWHYOYBTSZUQTSYLUVCWIYODTSZXJTSUVD
+      YOYHOTSUVEAYHYMYAAYHYDYJWJVKWKDOTWLWMUKWNWRDXJTTWOWMWPYBUQXHTTWQWMWSWTYNX
+      KUUMXAUUOYOXTUUTUUDWTXBXCXDXEXFXG $.
+  $}
+
+  ${
+    $d k x z A $.  $d k x z F $.  $d k x z N $.  $d k x z ph $.  $d k x z S $.
+    plycjlemc.n $e |- ( ph -> N e. NN0 ) $.
+    plycjlem.2 $e |- G = ( ( * o. F ) o. * ) $.
+    plycjlemc.a $e |- ( ph -> A : NN0 --> ( S u. { 0 } ) ) $.
+    plycjlemc.f $e |- ( ph -> F = ( z
+      e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) $.
+    plycjlemc.p $e |- ( ph -> F e. ( Poly ` S ) ) $.
+    $( Lemma for ~ plycj .  (Contributed by Mario Carneiro, 24-Jul-2014.)
+       (Revised by Jim Kingdon, 22-Sep-2025.) $)
+    plycjlemc $p |- ( ph -> G = ( z e. CC |->
+        sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) ) $=
+      ( cc co cfv ccj cexp cmul wcel vx cc0 cfz cv csu cmpt ccom cjcl adantl wf
+      cjf a1i feqmptd wa cfn 0zd nn0zd fzfigd adantr cn0 csn cun wss plybss syl
+      cply snssi mp1i unssd fssd elfznn0 ffvelcdmd adantlr simplr expcld mulcld
+      0cn fsumcl wceq oveq1 oveq2d sumeq2sdv cbvmptv eqtrdi fveq2 fmptco fveq2d
+      eqtrid ad2antlr fsumcj cjmuld syl2anc cjexpd oveq1d eqtr2d oveq12d eqtr4d
+      fvco3 cjcj sumeq2dv eqtrd mpteq2dva ) AGBNUBHUCOZEUDZCPZBUDZQPZXDROZSOZEU
+      EZQPZUFZBNXCXDQCUGPZXFXDROZSOZEUEZUFAGQFUGZQUGXLJABUANNXGXCXEUAUDZXDROZSO
+      ZEUEZQPZXKQXQXFNTZXGNTZAXFUHZUIABNNQNNQUJAUKULUMZAUABNNYAXGYBFQAXRNTZUNZX
+      CXTEAXCUOTZYGAUBHAUPAHIUQURZUSYHXDXCTZUNZXEXSAYKXENTZYGAYKUNUTNXDCAUTNCUJ
+      ZYKAUTDUBVAZVBNCKADYONAFDVFPTDNVCMDFVDVEUBNTYONVCAVQUBNVGVHVIVJUSZYKXDUTT
+      ZAXDHVKZUIVLZVMYLXRXDAYGYKVNYKYQYHYRUIVOVPVRAFBNXCXEXNSOZEUEZUFUANYAUFLBU
+      ANUUAYAXFXRVSZXCYTXTEUUBXNXSXESXFXRXDRVTWAWBWCWDYFXFYAQWEWFXRXGVSZYAXJQUU
+      CXCXTXIEUUCXSXHXESXRXGXDRVTWAWBWGWFWHABNXKXPAYCUNZXKXCXIQPZEUEXPUUDXCXIEA
+      YIYCYJUSUUDYKUNZXEXHAYKYMYCYSVMZUUFXGXDYCYDAYKYEWIZYKYQUUDYRUIZVOZVPWJUUD
+      XCUUEXOEUUFUUEXEQPZXHQPZSOXOUUFXEXHUUGUUJWKUUFXMUUKXNUULSUUFYNYQXMUUKVSAY
+      KYNYCYPVMUUIUTNXDQCWRWLUUFUULXGQPZXDROXNUUFXGXDUUHUUIWMUUFUUMXFXDRYCUUMXF
+      VSAYKXFWSWIWNWOWPWQWTXAXBXA $.
+  $}
+
+  ${
+    $d A k x z $.  $d F a k n x z $.  $d G a n $.  $d N k x z $.
+    $d S a k n x z $.  $d a j k n w z $.  $d a k n ph x z $.
+    plycj.2 $e |- G = ( ( * o. F ) o. * ) $.
+    plycj.3 $e |- ( ( ph /\ x e. S ) -> ( * ` x ) e. S ) $.
+    plycj.4 $e |- ( ph -> F e. ( Poly ` S ) ) $.
+    $( The double conjugation of a polynomial is a polynomial.  (The single
+       conjugation is not because our definition of polynomial includes only
+       holomorphic functions, i.e. no dependence on ` ( * `` z ) `
+       independently of ` z ` .)  (Contributed by Mario Carneiro,
+       24-Jul-2014.) $)
+    plycj $p |- ( ph -> G e. ( Poly ` S ) ) $=
+      ( vj vz vk cc cc0 cv co cfv cn0 wcel ccj cvv vw vn cfz cexp cmul csu cmpt
+      va wceq csn cun cmap wrex cply wa elply sylib simprd ccom simplrl simplrr
+      wss wf cnex a1i simpld ssexd ad2antrr c0ex snex unexg sylancl nn0ex mpbid
+      elmapd simpr oveq1 oveq2d sumeq2sdv cbvmptv fveq2 oveq12d cbvsumv mpteq2i
+      oveq2 eqtri eqtrdi plycjlemc snssi mp1i unssd adantr elfznn0 adantl fvco3
+      0cn syl2anc ffvelcdmd wi wo wral ralrimiva eleq1d rspccv syl elsni fveq2d
+      cj0 wb eqeltrdi elsng mpbird orim12d 3imtr4g ad3antrrr mpd eqeltrd elplyd
+      elun plyun0 eleqtrdi ex rexlimdvva ) ADUALMUBNZUCOZINZUHNZPZUANZYFUDOZUEO
+      ZIUFZUGZUIZUHCMUJZUKZQULOZUMUBQUMZECUNPZRZACLVBZYRADYSRZUUAYRUOHUACIUBDUH
+      UPUQZURAYNYTUBUHQYQAYDQRZYGYQRZUOZUOZYNYTUUGYNUOZEYPUNPZYSUUHEJLYEKNZSYGU
+      SPZJNZUUJUDOZUEOKUFUGUUIUUHJYGCKDEYDAUUDUUEYNUTZFUUHUUEQYPYGVCZAUUDUUEYNV
+      AUUHYPQYGTTUUHCTRZYOTRYPTRAUUPUUFYNACLTLTRAVDVEAUUAYRUUCVFZVGVHMVIVJCYOTT
+      VKVLQTRUUHVMVEVOVNZUUHDYMJLYEUUJYGPZUUMUEOZKUFZUGZUUGYNVPYMJLYEYHUULYFUDO
+      ZUEOZIUFZUGUVBUAJLYLUVEYIUULUIZYEYKUVDIUVFYJUVCYHUEYIUULYFUDVQVRVSVTJLUVE
+      UVAYEUVDUUTIKYFUUJUIYHUUSUVCUUMUEYFUUJYGWAYFUUJUULUDWEWBWCWDWFWGAUUBUUFYN
+      HVHWHUUHJUUKYPKYDAYPLVBUUFYNACYOLUUQMLRYOLVBAWPMLWIWJWKVHUUNUUHUUJYERZUOZ
+      UUKUUSSPZYPUVHUUOUUJQRZUUKUVIUIUUHUUOUVGUURWLZUVGUVJUUHUUJYDWMWNZQYPUUJSY
+      GWOWQUVHUUSYPRZUVIYPRZUVHQYPUUJYGUVKUVLWRAUVMUVNWSUUFYNUVGAUUSCRZUUSYORZW
+      TUVICRZUVIYORZWTUVMUVNAUVOUVQUVPUVRABNZSPZCRZBCXAUVOUVQWSAUWABCGXBUWAUVQB
+      UUSCUVSUUSUIUVTUVICUVSUUSSWAXCXDXEUVPUVRWSAUVPUVRUVIMUIZUVPUVIMSPMUVPUUSM
+      SUUSMXFXGXHWGZUVPUVILRUVRUWBXIUVPUVIMLUWCWPXJUVIMLXKXEXLVEXMUUSCYOXSUVICY
+      OXSXNXOXPXQXRXQCXTYAYBYCXP $.
+  $}
+
+  ${
+    $d A a k n x $.  $d F a k n x $.  $d G x $.  $d S x $.  $d V x $.
+    $( A polynomial with real coefficients distributes under conjugation.
+       (Contributed by Mario Carneiro, 24-Jul-2014.) $)
+    plyrecj $p |- ( ( F e. ( Poly ` RR ) /\ A e. CC ) ->
+                    ( * ` ( F ` A ) ) = ( F ` ( * ` A ) ) ) $=
+      ( vx vn vk va cr cfv wcel cc wa cc0 cv co cexp cmul wceq cn0 ccj adantr
+      cply cfz csu cmpt csn cun cmap wrex simpl elply sylib simprd simprl nn0zd
+      wss 0zd fzfigd wf simplrr cvv snssi ax-mp ssequn2 mpbi reex eqeltri nn0ex
+      0re elmap feq3 bitri elfznn0 adantl ffvelcdmd recnd simpllr expcld mulcld
+      fsumcj cjmuld simprr cjred cjexpd oveq12d eqtrd sumeq2dv simpr eqid oveq1
+      wb fveq1d oveq2d sumeq2sdv simplr fsumcl fvmptd3 cjcld 3eqtr4d rexlimdvva
+      fveq2d ex mpd ) BGUAHIZAJIZKZBCJLDMZUBNZEMZFMZHZCMZXHONZPNZEUCZUDZQZFGLUE
+      ZUFZRUGNZUHDRUHZABHZSHZASHZBHZQZXEGJUOZXTXEXCYFXTKXCXDUICGEDBFUJUKULXEXPY
+      EDFRXSXEXFRIZXIXSIZKZKZXPYEYJXPKZXGXJAXHONZPNZEUCZSHZXGXJYCXHONZPNZEUCZYB
+      YDYJYOYRQXPYJYOXGYMSHZEUCYRYJXGYMEYJLXFYJUPYJXFXEYGYHUMUNUQZYJXHXGIZKZXJY
+      LUUBXJUUBRGXHXIUUBYHRGXIURZXEYGYHUUAUSYHRXRXIURZUUCXRRXIXRGUTXQGUOZXRGQZL
+      GIUUEVHLGVAVBXQGVCVDZVEVFVGVIUUFUUDUUCWJUUGXRGRXIVJVBVKZUKUUAXHRIYJXHXFVL
+      VMZVNVOZUUBAXHXCXDYIUUAVPZUUIVQZVRZVSYJXGYSYQEUUBYSXJSHZYLSHZPNYQUUBXJYLU
+      UJUULVTUUBUUNXJUUOYPPUUBXJUUBRGXHXIYJUUCUUAYJYHUUCXEYGYHWAUUHUKTUUIVNWBUU
+      BAXHUUKUUIWCWDWEWFWETYKYAYNSYKYAAXOHZYNYKABXOYJXPWGZWKYJUUPYNQXPYJCAXNYNJ
+      XOJXOWHZXKAQZXGXMYMEUUSXLYLXJPXKAXHOWIWLWMXCXDYIWNZYJXGYMEYTUUMWOWPTWEWTY
+      KYDYCXOHZYRYKYCBXOUUQWKYJUVAYRQXPYJCYCXNYRJXOJUURXKYCQZXGXMYQEUVBXLYPXJPX
+      KYCXHOWIWLWMYJAUUTWQZYJXGYQEYTUUBXJYPUUJUUBYCXHYJYCJIUUAUVCTUUIVQVRWOWPTW
+      EWRXAWSXB $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#

mmil.raw.html

@@ -14433,6 +14433,21 @@
   and theorems</td>
 </tr>
 
+<tr>
+  <td>plycn</td>
+  <td><i>none</i></td>
+  <td>should be provable but needs a look through the continuity
+  theorems being used including expcn , mpomulcn , etc.  It should
+  be possible to replace the use of deg and coeff with ~ elply2</td>
+</tr>
+
+<tr>
+  <td>coecj</td>
+  <td>~ plycjlemc</td>
+  <td>the key difference between coecj and plycjlemc is that the latter
+  specifies coefficients explicitly</td>
+</tr>
+
 <tr>
   <td>fta1</td>
   <td><i>none</i></td>