Add fprodcl2lem to iset.mm

Stated as in set.mm.  The proof could be similar to the proof of
fsumcl2lem , which uses seq and some if statements.  But instead we
prove it by finite set induction and product notation directly, which
leads to a shorter proof (1490 bytes compressed compared with
2096 bytes compressed) which also is perhaps a bit clearer.

Author: jkingdon

iset.mm

@@ -124549,6 +124549,45 @@ seq n ( x. ,
       OVPVQVR $.
   $}
 
+  ${
+    fprodcllem.1 $e |- ( ph -> S C_ CC ) $.
+    fprodcllem.2 $e |- ( ( ph /\ ( x e. S /\ y e. S ) ) ->
+      ( x x. y ) e. S ) $.
+    fprodcllem.3 $e |- ( ph -> A e. Fin ) $.
+    fprodcllem.4 $e |- ( ( ph /\ k e. A ) -> B e. S ) $.
+
+    ${
+      $d A f k m x $.  $d A k w y z $.  $d B f m x $.  $d B u v y $.
+      $d B w y z $.  $d S f k x y $.  $d S k u v y $.  $d S k w y z $.
+      $d f k m ph x $.  $d ph w y z $.  $d u x y $.  $d v y z $.
+      fprodcl2lem.5 $e |- ( ph -> A =/= (/) ) $.
+      $( Finite product closure lemma.  (Contributed by Scott Fenton,
+         14-Dec-2017.)  (Revised by Jim Kingdon, 17-Aug-2024.) $)
+      fprodcl2lem $p |- ( ph -> prod_ k e. A B e. S ) $=
+        ( vz wcel c0 wceq cv eleq1d wa cmul vw vu vv cprod neneqd csn cun eqeq1
+        wo prodeq1 orbi12d eqidd orcd cfn wss cdif csb co nfcsb1v simplr simprr
+        eldifbd ad3antrrr simplll simplrl simpr sseldd syl2anc ad2antrr eldifad
+        simpll wral ralrimiva nfv nfel1 csbeq1a cbvral sylib r19.21bi fprodunsn
+        cc adantr c1 prodeq1d prod0 eqtrdi oveq1d mulid2d eqtrd eqeltrd olcd ex
+        ralrimivva oveq1 oveq2 cbvral2v wi rspc2v mpd findcard2sd orcomd ecased
+        jaod ) ADEGUDZFNZDOPZADOLUEAXFXEAUAQZOPZXGEGUDZFNZUIOOPZOEGUDZFNZUICQZO
+        PZXNEGUDZFNZUIXNMQZUFUGZOPZXSEGUDZFNZUIZXFXEUIUACMDXHXHXKXJXMXGOOUHXHXI
+        XLFXGOEGUJRUKXGXNPZXHXOXJXQXGXNOUHYDXIXPFXGXNEGUJRUKXGXSPZXHXTXJYBXGXSO
+        UHYEXIYAFXGXSEGUJRUKXGDPZXHXFXJXEXGDOUHYFXIXDFXGDEGUJRUKAXKXMAOULUMAXNU
+        NNZSZXNDUOZXRDXNUPZNZSZSZXOYCXQYMXOYCYMXOSZYBXTYNYAXPGXREUQZTURZFYMYAYP
+        PZXOYMXNXREYOGYJGXREUSZAYGYLUTYHYIYKVAZYMXRDXNYSVBYMGQZXNNZSZFWAEAFWAUO
+        ZYGYLUUAHVCUUBAYTDNEFNZAYGYLUUAVDUUBXNDYTYHYIYKUUAVEYMUUAVFVGKVHVGYMFWA
+        YOAUUCYGYLHVIYMAXRDNYOFNZAYGYLVKYMXRDXNYSVJAUUEMDAUUDGDVLUUEMDVLAUUDGDK
+        VMUUDUUEGMDUUDMVNGYOFYRVOYTXRPEYOFGXREVPZRVQVRVSVHZVGZUUFVTZWBYNYPYOFYN
+        YPWCYOTURYOYNXPWCYOTYNXPXLWCYNXNOEGYMXOVFWDEGWEWFWGYNYOYMYOWANXOUUHWBWH
+        WIYMUUEXOUUGWBWJWJWKWLYMXQYCYMXQSZYBXTUUJYAYPFYMYQXQUUIWBUUJUBQZUCQZTUR
+        ZFNZUCFVLUBFVLZYPFNZAUUOYGYLXQABQZXNTURZFNZCFVLBFVLUUOAUUSBCFFIWMUUSUUN
+        UUKXNTURZFNBCUBUCFFUUQUUKPUURUUTFUUQUUKXNTWNRXNUULPUUTUUMFXNUULUUKTWORW
+        PVRVCUUJXQUUEUUOUUPWQYMXQVFYMUUEXQUUGWBUUNUUPXPUULTURZFNUBUCXPYOFFUUKXP
+        PUUMUVAFUUKXPUULTWNRUULYOPUVAYPFUULYOXPTWORWRVHWSWJWKWLXCJWTXAXB $.
+    $}
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#