[add] assa2ass2; [shorten] assa2ass (#5009)

Author: zwang123

set.mm

@@ -284088,20 +284088,38 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     assa2ass.s $e |- .x. = ( .s ` W ) $.
     assa2ass.t $e |- .X. = ( .r ` W ) $.
     $( Left- and right-associative property of an associative algebra.  Notice
-       that the scalars are commuted!  (Contributed by AV, 14-Aug-2019.) $)
+       that the scalars are commuted!  (Contributed by AV, 14-Aug-2019.)
+       (Proof shortened by Zhi Wang, 11-Sep-2025.) $)
     assa2ass $p |- ( ( W e. AssAlg /\ ( A e. B /\ C e. B )
                     /\ ( X e. V /\ Y e. V ) ) ->
       ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( C .* A ) .x. ( X .X. Y ) ) ) $=
       ( wcel wa co casa wceq simp1 simpr 3ad2ant2 clmod assalmod simpl lmodvscl
       w3a syl3an 3ad2ant3 assaassr syl13anc assaass eqcomd lmodvsass oveq1d crg
-      3ad2ant1 assasca adantr adantl ringcl syl3anc 3adant3 eqtrd 3eqtrd ) IUAR
-      ZABRZCBRZSZJHRZKHRZSZUJZAJDTZCKDTETZCVQKETDTZCVQDTZKETZCAGTZJKETDTZVPVIVK
-      VQHRZVNVRVSUBVIVLVOUCZVLVIVKVOVJVKUDZUEZVIIUFRZVLVJVOVMWDIUGZVJVKUHZVMVNU
-      HZADFBHIJLMPNUIUKZVOVIVNVLVMVNUDULZCBDEFHIVQKLMNPQUMUNVPVIVKWDVNVSWAUBWEW
-      GWLWMVIVKWDVNUJSWAVSCBDEFHIVQKLMNPQUOUPUNVPWAWBJDTZKETZWCVPWHVKVJVMWAWOUB
-      VIVLWHVOWIUTWGVLVIVJVOWJUEVOVIVMVLWKULZWHVKVJVMUJSZVTWNKEWQWNVTCADGFBHIJL
-      MPNOUQUPURUNVPVIWBBRZVMVNWOWCUBWEVIVLWRVOVIVLSFUSRZVKVJWRVIWSVLFIMVAVBVLV
-      KVIWFVCVLVJVIWJVCBFGCANOVDVEVFWPWMWBBDEFHIJKLMNPQUOUNVGVH $.
+      3ad2ant1 assasca adantr adantl ringcld 3adant3 eqtrd 3eqtrd ) IUARZABRZCB
+      RZSZJHRZKHRZSZUJZAJDTZCKDTETZCVPKETDTZCVPDTZKETZCAGTZJKETDTZVOVHVJVPHRZVM
+      VQVRUBVHVKVNUCZVKVHVJVNVIVJUDZUEZVHIUFRZVKVIVNVLWCIUGZVIVJUHZVLVMUHZADFBH
+      IJLMPNUIUKZVNVHVMVKVLVMUDULZCBDEFHIVPKLMNPQUMUNVOVHVJWCVMVRVTUBWDWFWKWLVH
+      VJWCVMUJSVTVRCBDEFHIVPKLMNPQUOUPUNVOVTWAJDTZKETZWBVOWGVJVIVLVTWNUBVHVKWGV
+      NWHUTWFVKVHVIVNWIUEVNVHVLVKWJULZWGVJVIVLUJSZVSWMKEWPWMVSCADGFBHIJLMPNOUQU
+      PURUNVOVHWABRZVLVMWNWBUBWDVHVKWQVNVHVKSBFGCANOVHFUSRVKFIMVAVBVKVJVHWEVCVK
+      VIVHWIVCVDVEWOWLWABDEFHIJKLMNPQUOUNVFVG $.
+
+    $( Left- and right-associative property of an associative algebra.  Notice
+       that the scalars are not commuted!  (Contributed by Zhi Wang,
+       11-Sep-2025.) $)
+    assa2ass2 $p |- ( ( W e. AssAlg /\ ( A e. B /\ C e. B )
+                    /\ ( X e. V /\ Y e. V ) ) ->
+      ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( A .* C ) .x. ( X .X. Y ) ) ) $=
+      ( wcel wa co casa wceq simp1 simpl 3ad2ant2 3ad2ant3 clmod assalmod simpr
+      w3a 3ad2ant1 lmodvscld assaass syl13anc assaassr eqcomd lmodvsass assasca
+      oveq2d crg adantr adantl ringcld 3adant3 eqtrd 3eqtrd ) IUARZABRZCBRZSZJH
+      RZKHRZSZUJZAJDTCKDTZETZAJVOETDTZJAVODTZETZACGTZJKETDTZVNVGVHVKVOHRZVPVQUB
+      VGVJVMUCZVJVGVHVMVHVIUDZUEZVMVGVKVJVKVLUDUFZVNCDFBHIKLMPNVGVJIUGRZVMIUHUK
+      ZVJVGVIVMVHVIUIZUEZVMVGVLVJVKVLUIUFZULZABDEFHIJVOLMNPQUMUNVNVGVHVKWBVQVSU
+      BWCWEWFWLVGVHVKWBUJSVSVQABDEFHIJVOLMNPQUOUPUNVNVSJVTKDTZETZWAVNWGVHVIVLVS
+      WNUBWHWEWJWKWGVHVIVLUJSZVRWMJEWOWMVRACDGFBHIKLMPNOUQUPUSUNVNVGVTBRZVKVLWN
+      WAUBWCVGVJWPVMVGVJSBFGACNOVGFUTRVJFIMURVAVJVHVGWDVBVJVIVGWIVBVCVDWFWKVTBD
+      EFHIJKLMNPQUOUNVEVF $.
   $}
 
   ${