[shorten] asclelbas

Author: zwang123

discouraged

@@ -14677,6 +14677,7 @@ New usage of "anmp" is discouraged (11 uses).
 New usage of "aprilfools2025" is discouraged (0 uses).
 New usage of "archnq" is discouraged (1 uses).
 New usage of "arglem1N" is discouraged (0 uses).
+New usage of "asclelbasALT" is discouraged (0 uses).
 New usage of "atabs2i" is discouraged (1 uses).
 New usage of "atabsi" is discouraged (1 uses).
 New usage of "atbtwnexOLDN" is discouraged (0 uses).
@@ -19988,6 +19989,7 @@ Proof modification of "anabss7p1" is discouraged (5 steps).
 Proof modification of "ancomstVD" is discouraged (22 steps).
 Proof modification of "anmp" is discouraged (8 steps).
 Proof modification of "aprilfools2025" is discouraged (116 steps).
+Proof modification of "asclelbasALT" is discouraged (84 steps).
 Proof modification of "avril1" is discouraged (194 steps).
 Proof modification of "ax1" is discouraged (3 steps).
 Proof modification of "ax10fromc7" is discouraged (50 steps).

set.mm

@@ -835238,8 +835238,16 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     asclelbas.w $e |- ( ph -> W e. AssAlg ) $.
     asclelbas.c $e |- ( ph -> C e. B ) $.
     $( Lifted scalars are in the base set of the algebra.  (Contributed by Zhi
-       Wang, 11-Sep-2025.) $)
+       Wang, 11-Sep-2025.)  (Proof shortened by Thierry Arnoux,
+       22-Sep-2025.) $)
     asclelbas $p |- ( ph -> ( A ` C ) e. ( Base ` W ) ) $=
+      ( cbs cfv casa wcel crg assaring syl clmod assalmod eqid asclf ffvelcdmd
+      ) ACFLMZDBABUDECFGHAFNOZFPOJFQRAUEFSOJFTRIUDUAUBKUC $.
+
+    $( Alternate proof for ~ asclelbas .  (Contributed by Zhi Wang,
+       11-Sep-2025.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    asclelbasALT $p |- ( ph -> ( A ` C ) e. ( Base ` W ) ) $=
       ( cfv cur cvsca co cbs wcel wceq eqid syl asclval casa clmod assalmod crg
       assaring ringidcl 3syl lmodvscld eqeltrd ) ADBLZDFMLZFNLZOZFPLZADCQUKUNRK
       BUMULECFDGHIUMSZULSZUATADUMECUOFULUOSZHUPIAFUBQZFUCQJFUDTKAUSFUEQULUOQJFU