Add fsumcncntop to iset.mm

This is fsumcn from set.mm with a different notation for the topology of
the complex numbers.  The proof is similar to the set.mm proof.

Author: jkingdon

iset.mm

@@ -139380,6 +139380,53 @@ S C_ ( P ( ball ` D ) T ) ) $=
       YAUTYBYCYD $.
   $}
 
+  ${
+    $d k u v w x y z A $.  $d k v w x y z J $.  $d k z L $.  $d k w x y z ph $.
+    $d k v w x y z K $.  $d k u v w x y z X $.  $d k u v w x y z Y $.
+    $d u v w z B $.
+    fsumcncntop.3 $e |- K = ( MetOpen ` ( abs o. - ) ) $.
+    fsumcn.4 $e |- ( ph -> J e. ( TopOn ` X ) ) $.
+    fsumcn.5 $e |- ( ph -> A e. Fin ) $.
+    ${
+      $d y B $.
+      fsumcn.6 $e |- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) ) $.
+      $( A finite sum of functions to complex numbers from a common topological
+         space is continuous.  The class expression for ` B ` normally contains
+         free variables ` k ` and ` x ` to index it.  (Contributed by NM,
+         8-Aug-2007.)  (Revised by Mario Carneiro, 23-Aug-2014.) $)
+      fsumcncntop $p |- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) ) $=
+        ( vw csu cmpt wcel wceq cc wa caddc vy vz cv ccn co c0 csn cun mpteq2dv
+        sumeq1 eleq1d cc0 mpteq2i ctopon cfv cntoptopon a1i cnmptc syl5eqel cfn
+        sum0 0cnd wss cdif csb cin simplrr eldifbd disjsn sylibr simpllr unsnfi
+        wn eqidd syl3anc simp-4l simplrl eldifad snssd unssd sselda simplr wral
+        wi wf adantr cnf2 eqid fmpt rsp syl syl21anc fsumsplit simplll impancom
+        imp simpr ralrimiv syl2anc nfcsb1v nfel1 csbeq1a rspc sylc sumsns eqtrd
+        oveq2d mpteq2dva nfcv nfsum nfcsb nfov sumeq2ad csbeq2dv oveq12d cbvmpt
+        syl6eq ad3antrrr syl5eqelr simprr ralrimiva addcncntop cnmpt12f eqeltrd
+        nfmpt ctx ex findcard2sd ) ABHMUCZDENZOZFGUDUEZPBHUFDENZOZYLPBHUAUCZDEN
+        ZOZYLPZBHYOUBUCZUGZUHZDENZOZYLPZBHCDENZOZYLPMUAUBCYIUFQZYKYNYLUUGBHYJYM
+        YIUFDEUJUIUKYIYOQZYKYQYLUUHBHYJYPYIYODEUJUIUKYIUUAQZYKUUCYLUUIBHYJUUBYI
+        UUADEUJUIUKYICQZYKUUFYLUUJBHYJUUEYICDEUJUIUKAYNBHULOYLBHYMULDEVAUMABULF
+        GHRJGRUNUOPZAGIUPZUQAVBURUSAYOUTPZSZYOCVCZYSCYOVDZPZSZSZYRUUDUUSYRSZUUC
+        MHYOBYIDVEZENZEYSUVAVEZTUEZOZYLUUTUUCBHYPEYSDVEZTUEZOZUVEUUSUUCUVHQYRUU
+        SBHUUBUVGUUSBUCZHPZSZUUBYPYTDENZTUEUVGUVKYOYTDUUAEUVKYSYOPVMZYOYTVFUFQU
+        VKYSCYOUUNUUOUUQUVJVGZVHZYOYSVIVJUVKUUAVNUVKUUMUUQUVMUUAUTPAUUMUURUVJVK
+        UVNUVOYOYSUUPVLVOUVKEUCZUUAPZSAUVPCPZUVJDRPZAUUMUURUVJUVQVPUVKUUACUVPUV
+        KYOYTCUUNUUOUUQUVJVQUVKYSCUVKYSCYOUVNVRZVSVTWAUUSUVJUVQWBAUVRSZUVJUVSUW
+        AUVSBHWCZUVJUVSWDUWAHRBHDOZWEZUWBUWAFHUNUOPZUUKUWCYLPZUWDAUWEUVRJWFUUKU
+        WAUULUQLUWCFGHRWGVOBHRDUWCUWCWHWIVJUVSBHWJWKZWPWLWMUVKUVLUVFYPTUVKUUQUV
+        FRPZUVLUVFQUVNUVKYSCPZUVSECWCZUWHUVTUVKAUVJUWJAUUMUURUVJWNUUSUVJWQAUVJS
+        UVSECAUVRUVJUVSUWGWOWRWSUVSUWHEYSCEUVFREYSDWTZXAUVPYSQZDUVFREYSDXBZUKXC
+        XDDEYSUUPXEWSXGXFXHWFBMHUVGUVDMUVGXIBUVBUVCTBYOUVAEBYOXIBYIDWTZXJZBTXIB
+        EYSUVABYSXIUWNXKZXLUVIYIQZYPUVBUVFUVCTUWQYODUVAEBYIDXBZXMZUWQEYSDUVAUWR
+        XNZXOXPXQUUTMUVBUVCTFGGGHAUWEUUMUURYRJXRUUTMHUVBOYQYLBMHYPUVBMYPXIUWOUW
+        SXPUUSYRWQXSUUTMHUVCOBHUVFOZYLBMHUVFUVCMUVFXIUWPUWTXPUUTUWIUWFECWCZUXAY
+        LPZUUSUWIYRUUSYSCYOUUNUUOUUQXTVRWFAUXBUUMUURYRAUWFECLYAXRUWFUXCEYSCEUXA
+        YLEBHUVFEHXIUWKYEXAUWLUWCUXAYLUWLBHDUVFUWMUIUKXCXDXSTGGYFUEGUDUEPUUTGIY
+        BUQYCYDYGKYH $.
+    $}
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

mmil.raw.html

@@ -10724,8 +10724,7 @@
 
 <tr>
   <td>fsumcn</td>
-  <td><i>none</i></td>
-  <td>the set.mm proof uses addcn</td>
+  <td>~ fsumcncntop</td>
 </tr>
 
 <tr>