eliminated txpssvvv and thus all occurrences of _V X. _V

ZhihanLiphys · Apr 19, 2021 · 31d6e1a · 31d6e1a
1 parent b340435
commit 31d6e1a
Showing 1 changed file with 15 additions and 36 deletions.
diff --git a/nf.mm b/nf.mm
@@ -54996,19 +54996,6 @@ result of an operator (deduction version).  (Contributed by Paul
       ( cvv wcel cimage imageexg ax-mp ) ACDAECDBACFG $.
   $}
 
-  ${
-    $d R x y z $.
-    $( Subset law for tail cross product.  (Contributed by SF, 18-Feb-2015.) $)
-    txpssvvv $p |- ( R (x) S ) C_ ( _V X. ( _V X. _V ) ) $=
-      ( vx vy vz ctxp c1st ccnv ccom c2nd cvv cxp cv wbr wex cop opelxp exlimiv
-      wcel vex cin df-txp inss1 wa wceq brcnv br1st bitri mpbir2an eleq1 mpbiri
-      sylbi adantl opelco mpbiran 3imtr4i relssi sstri eqsstri ) ABFGHZAIZJHBIZ
-      UAZKKKLZLZABUBVCVAVEVAVBUCCDVAVECMZEMZANZVGDMZUTNZUDZEOVIVDSZVFVIPZVASVMV
-      ESZVKVLEVJVLVHVJVIVGVFPZUEZCOZVLVJVIVGGNVQVGVIGUFCVIVGETZUGUHVPVLCVPVLVOV
-      DSZVSVGKSVFKSZVRCTZVGVFKKQUIVIVOVDUJUKRULUMREVFVIUTAUNVNVTVLWAVFVIKVDQUOU
-      PUQURUS $.
-  $}
-
   ${
     $d p x $.  $d p y $.  $d p z $.  $d R p $.  $d R x $.  $d R y $.  $d R z $.
     $d S p $.  $d S x $.  $d S y $.  $d S z $.  $d x y $.  $d x z $.  $d y z $.
@@ -55034,29 +55021,21 @@ result of an operator (deduction version).  (Contributed by Paul
     $( Composition distributes over tail cross product in the case of a
        function.  (Contributed by SF, 18-Feb-2015.) $)
     txpcofun $p |- ( ( R (x) S ) o. F ) = ( ( R o. F ) (x) ( S o. F ) ) $=
-      ( vx vy vz vv vu wceq cv wcel wb cvv wss cdm cop wex wbr wa ctxp ccom cxp
-      vt vs wral crn ssdmrn ssv rncoss txpssvvv ax-mp rnxpss sstri xpss12 mp2an
-      rnss ssofeq wrex elxp2 rexv opeq2 eqeq2d rexxp exbii 3bitri dmcoss opeldm
-      sseldi df-br cin dmtxp inss1 eqsstri breldm sylbir trtxp anbi2i anass cfv
-      bitr4i wfun wi funbrfv fvex breq1 ceqsexv eqcom mpan syl5bb anbi1d exbidv
-      funbrfvb syl5bbr bibi1d syl5ibcom adantrd pm5.32d anbi12i oteltxp 3bitr4i
-      syl5 opelco 19.41v 3bitr4g pm5.21nii eleq1 bibi12d exlimiv exlimivv sylbi
-      mpbiri mprgbir ) ABUAZCUBZACUBZBCUBZUAZJZUDKZXOLZXTXRLZMZUDNNNUCZUCZXOYEO
-      XRYEOXSYCUDYEUFMXOXOPZXOUGZUCZYEXOUHYFNOYGYDOYHYEOYFUIYGXNUGZYDXNCUJYIYEU
-      GZYDXNYEOYIYJOABUKXNYEUQULNYDUMUNUNYFNYGYDUOUPUNXPXQUKUDXOXRYEURUPXTYELZX
-      TEKZFKZGKZQZQZJZGRZFRZERZYCYKXTYLUEKZQZJZUEYDUSZENUSUUDERYTEUEXTNYDUTUUDE
-      VAUUDYSEUUDYQGNUSZFNUSUUEFRYSUUCYQUEFGNNUUAYOJUUBYPXTUUAYOYLVBVCVDUUEFVAU
-      UEYRFYQGVAVEVFVEVFYRYCEFYQYCGYQYCYPXOLZYPXRLZMUUFYLCPZLZUUGUUFYFUUHYLXNCV
-      GYLYOXOVHVIUUGYLYOXRSZUUIYLYOXRVJUUJXRPZUUHYLUUKXPPZXQPZVKZUUHXPXQVLUUNUU
-      LUUHUULUUMVMACVGUNVNYLYOXRVOVIVPUUIYLHKZCSZUUOYOXNSZTZHRUUPUUOYMASZTZYLIK
-      ZCSZUVAYNBSZTZIRZTZHRZUUFUUGUUIUURUVFHUURUUTUUOYNBSZTZUUIUVFUURUUPUUSUVHT
-      ZTUVIUUQUVJUUPUUOYMYNABVQVRUUPUUSUVHVSWAUUIUUTUVHUVEUUIUUPUVHUVEMZUUSUUPY
-      LCVTZUUOJZUUIUVKCWBZUUPUVMWCDYLUUOCWDULUUIUVLYNBSZUVEMUVMUVKUVOUVAUVLJZUV
-      CTZIRUUIUVEUVCUVOIUVLYLCWEUVAUVLYNBWFWGUUIUVQUVDIUUIUVPUVBUVCUVPUVLUVAJZU
-      UIUVBUVAUVLWHUVNUUIUVRUVBMDYLUVACWMWIWJWKWLWNUVMUVOUVHUVEUVLUUOYNBWFWOWPX
-      BWQWRWJWLHYLYOXNCXCYLYMQXPLZYLYNQXQLZTUUTHRZUVETUUGUVGUVSUWAUVTUVEHYLYMAC
-      XCIYLYNBCXCWSYLYMYNXPXQWTUUTUVEHXDXAXEXFYQYAUUFYBUUGXTYPXOXGXTYPXRXGXHXLX
-      IXJXKXM $.
+      ( vx vt vy vz ccom cv cop wceq wex wcel wb ax-mp wbr wa breq1 opelco ctxp
+      cvv vex opeqex cdm cfv dmcoss opeldm sseldi pm4.71ri anbi1i anass ceqsexv
+      fvex anbi12i eqcom funbrfvb syl5bb anbi1d exbidv syl6bbr anbi12d syl5rbbr
+      wfun mpan pm5.32i 3bitrri 19.41v wi funbrfv trtxp syl exbii 3bitr4i bitri
+      eldm oteltxp opeq2 eleq1d bibi12d mpbiri exlimivv eqrelriv ) EFABUAZCIZAC
+      IZBCIZUAZFJZGJZHJZKZLZHMGMZEJZWIKZWENZWPWHNZOZWIUBNWNFUCGHWIUBUDPWMWSGHWM
+      WSWOWLKZWENZWTWHNZOWOCUEZNZWOCUFZWJAQZXEWKBQZRZRZWOWJKWFNZWOWKKWGNZRZXAXB
+      XLXDXJRZXKRXDXLRXIXJXMXKXJXDXJWFUEXCWOACUGWOWJWFUHUIUJUKXDXJXKULXDXLXHXHW
+      IXELZWIWJAQZRZFMZXNWIWKBQZRZFMZRXDXLXQXFXTXGXOXFFXEWOCUNZWIXEWJASUMXRXGFX
+      EYAWIXEWKBSUMUOXDXQXJXTXKXDXQWOWICQZXORZFMXJXDXPYCFXDXNYBXOXNXEWILZXDYBWI
+      XEUPCVDZXDYDYBODWOWICUQVEURZUSUTFWOWJACTVAXDXTYBXRRZFMXKXDXSYGFXDXNYBXRYF
+      USUTFWOWKBCTVAVBVCVFVGXAYBWIWLWDQZRZFMZXIFWOWLWDCTYBXHRZFMYBFMZXHRYJXIYBX
+      HFVHYIYKFYBYHXHYBYDYHXHOYEYBYDVIDWOWICVJPXHXEWLWDQYDYHXEWJWKABVKXEWIWLWDS
+      VCVLVFVMXDYLXHFWOCVPUKVNVOWOWJWKWFWGVQVNWMWQXAWRXBWMWPWTWEWIWLWOVRZVSWMWP
+      WTWHYMVSVTWAWBPWC $.
   $}
 
   ${