diff --git a/set.mm b/set.mm
index 4e191bafe..155274731 100644
--- a/set.mm
+++ b/set.mm
@@ -635137,7 +635137,7 @@ x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ) $=
       clmod lspprcl simpr lspprid2 lspprss sspss sylib clvec dvhlvec lspprat wi
       csn w3a chlt 3ad2ant1 simp2 dvh3dim2 clsm csubg lsssssubg lspsncl syl2anc
       syl sseldd prssi snsspr1 lspss syl3anc simp3 sseqtrd lsmless2 lsmpr prcom
-      co a1i fveq2i syl5eq 3sstr4d ssneld snsspr2 anim12d reximdv rexlimdv3a wb
+      co a1i fveq2i eqtrid 3sstr4d ssneld snsspr2 anim12d reximdv rexlimdv3a wb
       mpd eleq2i notbii eleq2 notbid anbi12d rexbidv mpbid jaodan syldan cplusg
       simpl1l simpl2 lmodvacl simpl3l sylnib lssvancl2 simpl1r lssvancl1 rspcev
       eleq1 syl12anc pm2.61dan ) AKLCUCGUDZUEZBUFZJKUCZGUDZUEZUGZYGYEUEZUGZUHZB
@@ -635896,7 +635896,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
       ( cfv wceq wss vw wcel cvv cv csn w3a wi wal wa wral cmap crab elex clpoN
       cpw co cbs c0g clsh clsa fveq2 eqtr4di pweqd oveq12d fveq2d sneqd eqeq12d
       sseq2d 3anbi12d imbi1d 2albidv eleq2d anbi1d raleqbidv 3anbi123d df-lpolN
-      clss rabeqbidv ovex rabex fvmpt syl5eq syl ) IJUBIUCUBZDHFUDZRZKUEZSZAUDZ
+      clss rabeqbidv ovex rabex fvmpt eqtrid syl ) IJUBIUCUBZDHFUDZRZKUEZSZAUDZ
       HTZBUDZHTZWIWKTZUFZWKWERWIWERZTZUGZBUHAUHZWOGUBZWOWERWISZUIZACUJZUFZFEHUO
       ZUKUPZULZSIJUMWDDIUNRXFQUAIUAUDZUQRZWERZXGURRZUEZSZWIXHTZWKXHTZWMUFZWPUGZ
       BUHAUHZWOXGUSRZUBZWTUIZAXGUTRZUJZUFZFXGVQRZXHUOZUKUPZULXFUCUNXGISZYCXCFYF
@@ -636801,7 +636801,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
         ( wcel co cfv wceq clmod clvec lveclmod syl lmodgrp cbs crg ldualvaddcl
         cgrp lmodring lflcl syl3anc cdr wne lvecdrng drnginvrcl ringcl lmodvscl
         eqid grpsubcl eqeltrid fveq2i csg lflsub syl112anc cur ringass syl13anc
-        lflmul drnginvrl oveq2d ringridm syl2anc 3eqtrd ringgrp grpsubid syl5eq
+        lflmul drnginvrl oveq2d ringridm syl2anc 3eqtrd ringgrp grpsubid eqtrid
         eqtrd jca ) ABNUOBIKDUPZUQZQURABOOWRUQZPWRUQZLUQZGUPZPFUPZMUPZNUMAHVGUO
         ZONUOZXDNUOZXENUOAHUSUOZXFAHUTUOZXIULHVAVBZHVCVBUHAXIXCEVDUQZUOZPNUOZXH
         XKAEVEUOZWTXLUOZXBXLUOZXMAXIXOXKEHTVHVBZAXJWRJUOZXGXPULACDJIKHUEUFUGXKU
@@ -636979,7 +636979,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
       lclkrlem2v $p |- ( ph -> ( L ` ( E .+ G ) ) = V ) $=
         ( co cfv dvhlmod ldualvaddcl lkrssv cpr clss eqid lspprcl cdih crn wcel
         wceq dihprrn wss lssss syl dochoccl mpbid dochexmid dvhlvec cin csn cun
-        lclkrlem2n wa snssd dochdmj1 syl3anc df-pr fveq2i unssd dochocsp syl5eq
+        lclkrlem2n wa snssd dochdmj1 syl3anc df-pr fveq2i unssd dochocsp eqtrid
         chlt ineq12d 3eqtr4d lkrin eqsstrd csubg clmod lsssssubg sseldd dochlss
         wb syl2anc lkrlss lsmlub mpbi2and eqsstrrd eqssd ) AIKCVIZOVJZSAJXTOSHU
         DUKUSAHLNTUTVBVDVKZABCJIKHUKULUMYBUPUQVLZVMASUAUBVNZQVJZYERVJZDVIZYAADH
@@ -637321,7 +637321,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
       wss clmod dvhlmod clss lduallmod ldualelvbase lspsncl syl2anc lssel sylan
       wceq ldualvbase eleqtrd cvsca co csca wb lspsnel ldualsbase rexeqdv bitrd
       lkrssv biimpa clvec dvhlvec lkrss2N mpbird dochss syl3anc sseld ex syl5bi
-      rexlimdv lspsnid eleqtrrdi 2fveq3 eleq2d rspcev impbid syl5bb syl5eq
+      rexlimdv lspsnid eleqtrrdi 2fveq3 eleq2d rspcev impbid syl5bb eqtrid
       eqrdv ) ACFDFUHZKUIZMUIZUJZHKUIZMUIZUDAUFXGXIUFUHZXGUKXJXFUKZFDULZAXJXIUK
       ZFXJDXFUMAXLXMAXKXMFDXDDUKXDHUNLUIZUKZAXKXMUOZDXNXDUEUPAXOXPAXOUQZXFXIXJX
       QJURUKNIUKUQZXEEUSUIZVBXHXEVBZXFXIVBAXRXOUBUTXQGXDKXSEXSVAZRSAEVCUKXOAEIJ
@@ -637358,7 +637358,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
       ( cfv co fveq1i csg eqid clvec wcel clmod lveclmod syl cbs lvecdrng lflcl
       cdr wne syl3anc drnginvrcl lmodmcl ldualvscl ldualvsubval ldualvsval wceq
       cur drnginvrr oveq1d crg lmodring ringass syl13anc ringlidm syl2anc eqtrd
-      3eqtr3d oveq2d cgrp lmodfgrp grpsubid 3eqtrd syl5eq ) ANJUKNGNIUKZKUKZNGU
+      3eqtr3d oveq2d cgrp lmodfgrp grpsubid 3eqtrd eqtrid ) ANJUKNGNIUKZKUKZNGU
       KZEULZIDULZLULZUKZONJWOUJUMAWPWLNWNUKZCUNUKZULWLWLWRULZOABCWRHGWNLMFNPQWR
       UOZUAUBUDAFUPUQZFURUQZUEFUSUTZUFABCDHICVAUKZFWMUAQXDUOZUBUCXCAXBWKXDUQZWL
       XDUQZWMXDUQXCACVDUQZWJXDUQZWJOVEZXFAXAXHUECFQVBUTZAXAIHUQNMUQZXIUEUGUHCHI
@@ -637609,7 +637609,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
          by NM, 22-Feb-2015.) $)
       lcf1o $p |- ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) ) $=
         ( vy vz vu vl csn cdif cv co wceq cfv wrex crio cmpt weq oveq1 cbvrexvw
-        eqeq2d oveq2d rexbidv syl5bb cbvriotavw riotabidv syl5eq cbvmptv fveq2d
+        eqeq2d oveq2d rexbidv syl5bb cbvriotavw riotabidv eqtrid cbvmptv fveq2d
         eqeq1 sneq oveq2 rexeqbidv mpteq2dv eqtri lcfrlem9 ) AUTVAVBEFGHIJKLMVC
         OPQRSTUAUBUCUDUEUFUGUHUIUJUKULUMUNUOUPUQQBUAUCVDVEZDUADVFZCVFZNVFZBVFZK
         VGZGVGZVHZCWPVDZTVIZVJZNIVKZVLZVLUTWLVBUAVBVFZVAVFZVCVFZUTVFZKVGZGVGZVH
@@ -637743,7 +637743,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
     lcfrlem18 $p |- ( ph
   -> ( ._|_ ` { X , Y } ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) ) $=
       ( cpr cfv csn cun cin df-pr fveq2i chlt wcel wa wss wceq eldifad dochdmj1
-      snssd syl3anc syl5eq ) AKLUFZHUGKUHZLUHZUIZHUGZVDHUGVEHUGUJZVCVFHKLUKULAF
+      snssd syl3anc eqtrid ) AKLUFZHUGKUHZLUHZUIZHUGZVDHUGVEHUGUJZVCVFHKLUKULAF
       UMUNJEUNUOVDIUPVEIUPVGVHUQUBAKIAKIMUHZUCURUTALIALIVIUDURUTDEFHIJVDVENPQOU
       SVAVB $.
 
@@ -637804,7 +637804,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
          -> ( ( ._|_ ` { X , Y } ) .(+) B ) = ( ._|_ ` { ( X .+ Y ) } ) ) $=
         ( csn cfv co cin cpr fveq2i cdjh cdih eqid eldifad dihprrn chlt wcel wa
         wss crn clmod dvhlmod lmodvacl syl3anc dochcl syl2anc dochdmm1 dochocsn
-        snssd oveq2d prssi lspssv 3eqtrd syl5eq ineq2d csubg wceq lsssssubg syl
+        snssd oveq2d prssi lspssv 3eqtrd eqtrid ineq2d csubg wceq lsssssubg syl
         dihjat1 clss lspsncl lsmcl sseldd dochlss lspsntri lsmmod2 lsmpr ineq1d
         lspprcl dochnoncon eqtr3d oveq1d lsm02 eqtrd fveq2d dihsmsnrn lcfrlem22
         syl31anc lsatssv dochocsp dih1dimat dochoc oveq12d dihjat2 3eqtr3d ) AM
@@ -638014,7 +638014,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
         ( vf cfv c0g cmulr co cvsca oveq2d crg wcel wceq clmod dvhlmod lmodring
         syl cdr clvec dvhlvec lvecdrng clfn cv crab lcfrlem10 lcfrlem22 lsatssv
         wne eqid sseldd lflcl syl3anc drnginvrcl ringrz syl2anc oveq1d ldual0vs
-        eqtrd cgrp cbs ldualgrp ldualelvbase grpsubid1 syl5eq csn cdif eldifsni
+        eqtrd cgrp cbs ldualgrp ldualelvbase grpsubid1 eqtrid csn cdif eldifsni
         lcfrlem13 eqnetrd ) AGUGSVQZHVRVQZAGYBRUHSVQZVQZPVQZRYBVQZLVSVQZVTZYDHW
         AVQZVTZUBVTZYBVNAYLYBYCUBVTZYBAYKYCYBUBAYKJYDYJVTYCAYIJYDYJAYIYFJYHVTZJ
         AYGJYFYHVOWBALWCWDZYFKWDZYNJWEANWFWDZYOANQTUFUJULURWGZLNVDWHWIALWJWDZYE
@@ -638331,7 +638331,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
     lcdval $p |- ( ph -> C = ( D |`s { f e. F
             | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } ) ) $=
       ( vw wcel wa cfv wceq crab cress cdvh cld clk coch clfn cmpt clcd lcdfval
-      cv co fveq1d syl5eq eqtr4di fveq2d fveq12d eqeq12d rabeqbidv oveq12d eqid
+      cv co fveq1d eqtrid eqtr4di fveq2d fveq12d eqeq12d rabeqbidv oveq12d eqid
       fveq2 ovex fvmpt sylan9eq syl ) AHLUBZKGUBZUCBCEUPZIUDZJUDZJUDZVOUEZEFUFZ
       UGUQZUETVLVMBKUAGUAUPZHUHUDZUDZUIUDZVNWCUJUDZUDZWAHUKUDZUDZUDZWHUDZWFUEZE
       WCULUDZUFZUGUQZUMZUDZVTVLBKHUNUDZUDWPOVLKWQWOUAEGHLMUOURUSUAKWNVTGWOWAKUE
@@ -638383,7 +638383,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
     $( Vector base set of a dual vector space of functionals with closed
        kernels.  (Contributed by NM, 13-Mar-2015.) $)
     lcdvbase $p |- ( ph -> V = B ) $=
-      ( cld cfv cress co cbs chlt eqid lcdval2 fveq2d syl5eq wss wceq cv ssrab2
+      ( cld cfv cress co cbs chlt eqid lcdval2 fveq2d eqtrid wss wceq cv ssrab2
       crab eqsstri clmod dvhlmod ldualvbase sseqtrrid ressbas2 syl eqtr4d ) AKD
       UBUCZBUDUEZUFUCZBAKCUFUCVGPACVFUFABCVEDEFGHIJLUGMNOQRSVEUHZUATUIUJUKABVEU
       FUCZULBVGUMAFBVIBEUNIUCZJUCJUCVJUMZEFUPFTVKEFUOUQAVEFVIDURRVHVIUHZADGHLMQ
@@ -638484,7 +638484,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
        NM, 16-Mar-2015.)  (Revised by Mario Carneiro, 6-May-2015.) $)
     lcdsca $p |- ( ph -> R = O ) $=
       ( vf csca cfv eqid cld cv coch wceq clfn crab cress co chlt lcdval fveq2d
-      clk cvv wcel fvex rabex resssca ax-mp eqtr4di clmod ldualsca eqtrd syl5eq
+      clk cvv wcel fvex rabex resssca ax-mp eqtr4di clmod ldualsca eqtrd eqtrid
       dvhlmod ) ACBRSZHOAVEDUASZRSZHAVEVFQUBDULSZSZIGUCSSZSVJSVIUDZQDUESZUFZUGU
       HZRSZVGABVNRABVFDQVLFGVHVJIUIJVJTNKVLTVHTVFTZPUJUKVMUMUNVGVOUDVKQVLDUEUOU
       PVMVGVFVNUMVNTVGTZUQURUSAVFVGEHDUTLMVPVQADFGIJKPVDVAVBVC $.
@@ -638537,7 +638537,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
     $( Scalar multiplication for the closed kernel vector space dual.
        (Contributed by NM, 20-Mar-2015.) $)
     lcdsmul $p |- ( ph -> ( X .xb Y ) = ( Y .x. X ) ) $=
-      ( co coppr cfv cmulr eqid lcdsca fveq2d syl5eq oveqd opprmul eqtrdi ) ALM
+      ( co coppr cfv cmulr eqid lcdsca fveq2d eqtrid oveqd opprmul eqtrdi ) ALM
       DUELMGUFUGZUHUGZUEMLEUEADUQLMADCUHUGUQUAACUPUHABCFGHIUPKNOPUPUIZSTUBUJUKU
       LUMJGUQEUPLMQRURUQUIUNUO $.
   $}
@@ -638708,7 +638708,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
        (Contributed by NM, 20-Mar-2015.) $)
     lcd0v $p |- ( ph -> O = ( V X. { .0. } ) ) $=
       ( cfv eqid vf cld cv clk coch wceq clfn crab cress co c0g csn chlt lcdval
-      cxp fveq2d syl5eq clmod wcel clss dvhlmod lduallmod lclkr syl2anc ldual0v
+      cxp fveq2d eqtrid clmod wcel clss dvhlmod lduallmod lclkr syl2anc ldual0v
       lss0v 3eqtrd ) AGDUBSZUAUCDUDSZSZIFUESSZSVKSVJUFUADUGSZUHZUIUJZUKSZVHUKSZ
       HJULUOAGBUKSVOQABVNUKABVHDUAVLEFVIVKIUMKVKTZPLVLTZVITZVHTZRUNUPUQAVHURUSV
       MVHUTSZUSVOVPUFAVHDVTADEFIKLRVAZVBAVMVHWADUAVLEFVIVKIKLVQVRVSVTWATZVMTRVC
@@ -638874,7 +638874,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
     $( Subspaces of a dual vector space of functionals with closed kernels.
        (Contributed by NM, 13-Mar-2015.) $)
     lcdlss $p |- ( ph -> S = ( T i^i ~P B ) ) $=
-      ( vu cpw cin cv wcel wss cress clss cfv chlt lcdval2 fveq2d syl5eq eleq2d
+      ( vu cpw cin cv wcel wss cress clss cfv chlt lcdval2 fveq2d eqtrid eleq2d
       wa co clmod dvhlmod lduallmod lclkr eqid lsslss syl2anc bitrd elin anbi2i
       wb velpw bitr2i bitrdi eqrdv ) AUFEFBUGZUHZAUFUIZEUJZVSFUJZVSBUKZUTZVSVRU
       JZAVTVSDBULVAZUMUNZUJZWCAEWFVSAECUMUNWFRACWEUMABCDGHIJKLMNUOOPQSTUAUBUEUD
@@ -638915,7 +638915,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
     $( Span in the set of functionals with closed kernels.  (Contributed by NM,
        28-Mar-2015.) $)
     lcdlsp $p |- ( ph -> ( N ` G ) = ( M ` G ) ) $=
-      ( vf cfv cv clk coch wceq clfn crab cress clspn chlt lcdval fveq2d syl5eq
+      ( vf cfv cv clk coch wceq clfn crab cress clspn chlt lcdval fveq2d eqtrid
       co eqid fveq1d clmod wcel clss wss dvhlmod lduallmod lclkr sseqtrd lsslsp
       lcdvbase syl3anc eqtr4d ) AFJUBFCUAUCDUDUBZUBZKHUEUBUBZUBVLUBVKUFUADUGUBZ
       UHZUIUOZUJUBZUBZFIUBZAFJVPAJBUJUBVPRABVOUJABCDUAVMGHVJVLKUKLVLUPZPMVMUPZV
@@ -639026,7 +639026,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane).
      -> M = ( s e. S |-> { f e. F |
    ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( O ` ( L ` f ) ) C_ s ) } ) ) $=
       ( cfv vw wcel cv cdvh clss clk coch wceq wa clfn crab cmpt cmpd mapdffval
-      wss fveq1d syl5eq eqtr4di fveq2d fveq12d eqeq12d sseq1d anbi12d rabeqbidv
+      wss fveq1d eqtrid eqtr4di fveq2d fveq12d eqeq12d sseq1d anbi12d rabeqbidv
       fveq2 mpteq12dv eqid mptfvmpt sylan9eq ) FKUBZJEUBHJUAELUAUCZFUDTZTZUETZC
       UCZVMUFTZTZVKFUGTZTZTZVSTZVQUHZVTLUCZUOZUIZCVMUJTZUKZULZULZTZLAVOGTZITZIT
       ZWKUHZWLWCUOZUIZCDUKZULVJHJFUMTZTWJSVJJWRWIUACEFKLMUNUPUQLUAWQUEWIWHAEBJV
@@ -641775,7 +641775,7 @@ equations of part (5) in [Baer] p. 46, conjoined to share commonality in
     hvmapfval $p |- ( ph -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |->
      ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) ) $=
       ( vw wcel wa csn cdif cv co wceq cfv wrex crio cmpt cdvh cbs cvsca cplusg
-      c0g coch csca chvm hvmapffval fveq1d syl5eq fveq2 eqtr4di fveq2d difeq12d
+      c0g coch csca chvm hvmapffval fveq1d eqtrid fveq2 eqtr4di fveq2d difeq12d
       sneqd eqidd oveqd oveq123d eqeq2d rexeqbidv riotaeqbidv eqid fvexi difexi
       mpteq12dv mptex fvmpt sylan9eq syl ) AMEUKZQLUKZULNBPRUMZUNZCPCUOZDUOZKUO
       ZBUOZIUPZFUPZUQZDWSUMZOURZUSZKGUTZVAZVAZUQUIWLWMNQUJLBUJUOZMVBURZURZVCURZ
@@ -642030,7 +642030,7 @@ to provide a fixed reference vector (any other fixed vector would also
        map of the fiducial atom ` P = ( ( oc ` K ) ` W ) ` (see ~ dihpN ). @)
     eimval @p |- ( ph -> I = ( M ` <. ( _I |` B ) , ( _I |` T ) >. ) ) @=
       ( vw wcel cid cres cfv wa cop wceq cv cltrn chvm cmpt ceim eimfval fveq1d
-      syl5eq fveq2 eqtr4di eqidd reseq2d opeq12d fveq12d eqid fvex sylan9eq syl
+      eqtrid fveq2 eqtr4di eqidd reseq2d opeq12d fveq12d eqid fvex sylan9eq syl
       fvmpt ) AGBQZIEQZUAFRCSZRDSZUBZHTZUCOVCVDFIPEVERPUDZGUETZTZSZUBZVIGUFTZTZ
       TZUGZTZVHVCFIGUHTZTVRNVCIVSVQPCEGBJKUIUJUKPIVPVHEVQVIIUCZVMVGVOHVTVOIVNTH
       VIIVNULMUMVTVEVEVLVFVTVEUNVTVKDRVTVKIVJTDVIIVJULLUMUOUPUQVQURVGHUSVBUTVA
@@ -642084,7 +642084,7 @@ to provide a fixed reference vector (any other fixed vector would also
      chvm syl2anc lssel lcdvbaselfl dvhlmod lflcl syl3anc lcdvscl wne lcd0vvalN
       chlt fveq1 adantl simpr cv cvsca wrex wb lspsnel ad2antrr eqnetrrd simplr
       mpbid lvecvsn0 simpld jca ex reximdva mpd w3a cmulr simp3r 3ad2ant1 simp2
-     fveq2d lflmul cur fveq1i hvmapidN syl5eq oveq2d crg lmodring ringridm
+     fveq2d lflmul cur fveq1i hvmapidN eqtrid oveq2d crg lmodring ringridm
      3eqtrd
      syl112anc eqtrd simp3l eqnetrd rexlimdv3a necon2d lcdlkreqN sylanbrc eqidd
       eldifsn lcdlkreq2N eqtr4d lcdvsval oveq1d ringlidm 3eqtrrd eqlkr3 eqeq1d
@@ -642226,7 +642226,7 @@ first fundamental theorem of projective geometry (see ~ mapdpg ). @)
       ( vw va vu ve vn vf vc vm vj wcel wa cv csn cfv co wceq crio cif cmpt cbs
       cvsca csg cmpd wsbcSBC clspn clcd cdvh chvm cid cres cltrn cop cab
       hmapffval
-      fveq1d syl5eq wb fveq2 syl6reqr reseq2d opeq2d eqtr2id dfsbcqSBC syl
+      fveq1d eqtrid wb fveq2 syl6reqr reseq2d opeq2d eqtr2id dfsbcqSBC syl
       eqtr4di
       chma sbcbidvSBC bitrd cvv opex eqeltri w3a simp3 fveq2d fveq1 eqeq1d
       anbi12d
@@ -642461,7 +642461,7 @@ first fundamental theorem of projective geometry (see ~ mapdpg ). @)
             A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ) @=
       ( vw va vb vu vm wcel wa cv co cfv wceq wral crio cmpt clcd cbs chma
       wsbcSBC
-      cvsca csca cdvh cab cgma gmapffval fveq1d syl5eq fveq2 eqtr4di dfsbcqSBC
+      cvsca csca cdvh cab cgma gmapffval fveq1d eqtrid fveq2 eqtr4di dfsbcqSBC
       syl
       wb fveq2d oveqd eqeq2d ralbidv riotabidv mpteq2dv eleq2d sbcbidvSBC cvv
       fvex
@@ -643156,7 +643156,7 @@ first fundamental theorem of projective geometry (see ~ mapdpg ). @)
           = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) ) $=
       ( vw va vv vd vu vc vn vm vj wcel wa cxp cv c2nd cfv wceq csn c1st co cif
       crio cmpt c0g csg cmpd wsbc clspn cbs clcd cdvh chdma1 hdmap1ffval fveq1d
-      cab syl5eq fveq2 sbceq1d sbcbidv sbceqbid fvex wb eqeq2i biimpri 3ad2ant1
+      cab eqtrid fveq2 sbceq1d sbcbidv sbceqbid fvex wb eqeq2i biimpri 3ad2ant1
       simp2 fveq2d eqtrd eqtr4di simp3 id fveq1 eqeq1d anbi12d riotabidv ifeq2d
       w3a mpteq2dv eleq2d syl sbcie xpeq2 xpeq1d simp1 eqeq2d oveqd riotaeqbidv
       fveq12d ifeq12d mpteq12dv syl5bb syl3anc sbc3ie xpeq12d fveqeq2d ifbieq2d
@@ -644004,7 +644004,7 @@ first fundamental theorem of projective geometry (see ~ mapdpg ). @)
           y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ) $=
       ( vw va vv ve vu vi wcel wa cv csn cfv cun wn cotp wceq wi wral crio cmpt
       clspn chvm clcd cbs chdma1 wsbc cdvh cid cres cltrn cop hdmapffval fveq1d
-      cab chdma syl5eq fveq2 reseq2d opeq2d 2fveq3 oteq2d fveq2d eqeq2d ralbidv
+      cab chdma eqtrid fveq2 reseq2d opeq2d 2fveq3 oteq2d fveq2d eqeq2d ralbidv
       imbi2d riotaeqbidv mpteq2dv eleq2d sbceqbid sbcbidv opex fvex w3a eqtr4di
       wb simp1 simp2 simp3 eqtrd id fveq1 riotabidv syl sbcie fveq2i eqtr2i a1i
       sneqd fveq12d uneq12d notbid oteq1d fveq1i raleqbidv syl5bb sbc3ie bitrdi
@@ -645354,7 +645354,7 @@ fixed reference functional determined by this vector (corresponding to
     hgmapfval $p |- ( ph -> I = ( x e. B |-> ( iota_ y e. B
             A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ) $=
       ( vw va vb vu vm wcel wa cv cfv wceq wral crio cmpt cvsca clcd chdma wsbc
-      cbs csca cdvh cab chg hgmapffval fveq1d syl5eq fveq2 eqtr4di 2fveq3 oveqd
+      cbs csca cdvh cab chg hgmapffval fveq1d eqtrid fveq2 eqtr4di 2fveq3 oveqd
       co eqeq2d ralbidv riotabidv mpteq2dv eleq2d sbceqbid sbcbidv fvexi wb w3a
       simp2 simp1 fveq2d eqtrd simp3 fveq12d eqidd oveq123d eqeq12d riotaeqbidv
       fvex raleqbidv mpteq12dv syld3an2 sbc3ie bitrdi abbi1dv mptfvmpt sylan9eq
@@ -646076,7 +646076,7 @@ fixed reference functional determined by this vector (corresponding to
     hdmapip1 $p |- ( ph -> ( ( S ` X ) ` Y ) = .1. ) $=
       ( cfv co fveq2i cmulr cbs eqid csn eldifad cdr wcel c0g wne clvec dvhlvec
       lvecdrng syl hdmapipcl cdif eldifsni hdmapip0 necon3bid mpbird drnginvrcl
-      syl3anc hdmaplnm1 wceq drnginvrl eqtrd syl5eq ) AMLCUGZUGLVPUGZIUGZLDUHZV
+      syl3anc hdmaplnm1 wceq drnginvrl eqtrd eqtrid ) AMLCUGZUGLVPUGZIUGZLDUHZV
       PUGZFMVSVPUFUIAVTVRVQBUJUGZUHZFAVRBUKUGZBCDWAEGHJKLLOPQRTWCULZWAULZUCUDAL
       JNUMZUEUNZWGABUOUPZVQWCUPZVQBUQUGZURZVRWCUPAEUSUPWHAEGHKOPUDUTBETVAVBZAWC
       BCEGHJKLLOPQTWDUCUDWGWGVCZAWKLNURZALJWFVDUPWNUELJNVEVBAVQWJLNABCEGHJKLNWJ
@@ -646620,7 +646620,7 @@ fixed reference functional determined by this vector (corresponding to
       wa elex syl clh fvexi mptex nfcsb1v nfmpt fveq2 eqtr4di csbeq1a mpteq12dv
       nfcv df-hlhil fvmptf sylancl fvexd fveq2d simplr fveq12d sylan9eqr opeq2d
       id simpr oveq12d ad2antrr fveq1d mpoeq123dv preq12d uneq12d csbied simprd
-      tpeq123d tpex prex unex a1i fvmptd syl5eq ) ANPMUMUNZUNUOUPUNZOUQZUOURUNZ
+      tpeq123d tpex prex unex a1i fvmptd eqtrid ) ANPMUMUNZUNUOUPUNZOUQZUOURUNZ
       DUQZUOUSUNZEUQZUTZUOVAUNZGUQZUOVBUNZLUQZVCZVDZRAUIPUJMUKUIVFZUJVFZVEUNZUN
       ZULUKVFZUPUNZYAULVFZUQZYCYRURUNZUQZYEYNYOVGUNZUNZUOVHUNZYNYOVIUNZUNZUQZVJ
       VKZUQZUTZYHYRVAUNZUQZYJBCYTYTBVFZCVFZYNYOVLUNZUNZUNZUNZVMZUQZVCZVDZVNZVNZ
@@ -646701,7 +646701,7 @@ fixed reference functional determined by this vector (corresponding to
          28-Jun-2015.)  (Revised by AV, 6-Nov-2024.) $)
       hlhilslem $p |- ( ph -> C = ( F ` R ) ) $=
         ( cnx cfv eqid cstv chg cop csts co setsnid eqtri csca hlhilsca eqtr4di
-        fveq2d syl5eq ) ABERUASZIHUBSSZUCUDUEZFSZCFSBEFSUPQUNUMFEOPUFUGAUOCFAUO
+        fveq2d eqtrid ) ABERUASZIHUBSSZUCUDUEZFSZCFSBEFSUPQUNUMFEOPUFUGAUOCFAUO
         DUHSCAUODEUNGHIJLNKUNTUOTUIMUJUKUL $.
     $}
 
@@ -646715,7 +646715,7 @@ fixed reference functional determined by this vector (corresponding to
          (New usage is discouraged.)  (Proof modification is discouraged.) $)
       hlhilslemOLD $p |- ( ph -> C = ( F ` R ) ) $=
         ( cfv cnx cstv chg cop csts co ndxid wne c4 nnrei ltneii ndxarg neeq12i
-        starvndx mpbir setsnid eqtri csca eqid hlhilsca eqtr4di fveq2d syl5eq )
+        starvndx mpbir setsnid eqtri csca eqid hlhilsca eqtr4di fveq2d eqtrid )
         ABEUAUBTZJHUCTTZUDUEUFZFTZCFTBEFTVGSVEVDFEFIPQUGUAFTZVDUHIUIUHIUIIQUJRU
         KVHIVDUIFIPQULUNUMUOUPUQAVFCFAVFDURTCAVFDEVEGHJKMOLVEUSVFUSUTNVAVBVC $.
     $}
@@ -646786,7 +646786,7 @@ fixed reference functional determined by this vector (corresponding to
          (Contributed by NM, 22-Jun-2015.)  (Revised by Mario Carneiro,
          28-Jun-2015.) $)
       hlhilsbase2 $p |- ( ph -> C = ( Base ` R ) ) $=
-        ( cfv cbs chlt wcel cedring wa wceq dvhsca syl fveq2d syl5eq hlhilsbase
+        ( cfv cbs chlt wcel cedring wa wceq dvhsca syl fveq2d eqtrid hlhilsbase
         eqid eqtrd ) ABIGUAQQZRQZCRQABDRQULPADUKRAGSTIFTUBDUKUCOUKHDFGISJUKUIZK
         LUDUEUFUGAULCEUKFGIJUMMNOULUIUHUJ $.
     $}
@@ -646796,7 +646796,7 @@ fixed reference functional determined by this vector (corresponding to
       $( Scalar addition for the final constructed Hilbert space.  (Contributed
          by NM, 22-Jun-2015.)  (Revised by Mario Carneiro, 28-Jun-2015.) $)
       hlhilsplus2 $p |- ( ph -> .+ = ( +g ` R ) ) $=
-        ( cfv cplusg chlt wcel cedring wceq dvhsca syl fveq2d syl5eq hlhilsplus
+        ( cfv cplusg chlt wcel cedring wceq dvhsca syl fveq2d eqtrid hlhilsplus
         wa eqid eqtrd ) ABIGUAQQZRQZCRQABDRQULPADUKRAGSTIFTUHDUKUBOUKHDFGISJUKU
         IZKLUCUDUEUFAULCEUKFGIJUMMNOULUIUGUJ $.
     $}
@@ -646808,7 +646808,7 @@ fixed reference functional determined by this vector (corresponding to
          28-Jun-2015.) $)
       hlhilsmul2 $p |- ( ph -> .x. = ( .r ` R ) ) $=
         ( cfv cmulr chlt wcel cedring wa wceq dvhsca syl fveq2d hlhilsmul eqtrd
-        eqid syl5eq ) ADIGUAQQZRQZBRQADCRQULPACUKRAGSTIFTUBCUKUCOUKHCFGISJUKUIZ
+        eqid eqtrid ) ADIGUAQQZRQZBRQADCRQULPACUKRAGSTIFTUBCUKUCOUKHCFGISJUKUIZ
         KLUDUEUFUJABULEUKFGIJUMMNOULUIUGUH $.
     $}
 
@@ -646819,7 +646819,7 @@ fixed reference functional determined by this vector (corresponding to
          29-Jun-2015.) $)
       hlhils0 $p |- ( ph -> .0. = ( 0g ` R ) ) $=
         ( vx vy c0g cfv cbs eqidd eqid hlhilsbase2 cv cplusg hlhilsplus2 oveqdr
-        wcel wa grpidpropd syl5eq ) AICSTBSTPAQRCUATZCBAUMUBAUMBCDEFGHJKLMNOUMU
+        wcel wa grpidpropd eqtrid ) AICSTBSTPAQRCUATZCBAUMUBAUMBCDEFGHJKLMNOUMU
         CUDAQUEUMUIRUEUMUIUJQRCUFTZBUFTAUNBCDEFGHJKLMNOUNUCUGUHUKUL $.
     $}
 
@@ -646830,7 +646830,7 @@ fixed reference functional determined by this vector (corresponding to
          29-Jun-2015.)  (New usage is discouraged.) $)
       hlhils1N $p |- ( ph -> .1. = ( 1r ` R ) ) $=
         ( vx vy cur cfv cbs eqidd eqid hlhilsbase2 cv wcel wa hlhilsmul2 oveqdr
-        cmulr rngidpropd syl5eq ) AECSTBSTPAQRCUATZCBAUMUBAUMBCDFGHIJKLMNOUMUCU
+        cmulr rngidpropd eqtrid ) AECSTBSTPAQRCUATZCBAUMUBAUMBCDFGHIJKLMNOUMUCU
         DAQUEUMUFRUEUMUFUGQRCUJTZBUJTABCUNDFGHIJKLMNOUNUCUHUIUKUL $.
     $}
   $}
@@ -646900,7 +646900,7 @@ fixed reference functional determined by this vector (corresponding to
        by Mario Carneiro, 28-Jun-2015.) $)
     hlhilnvl $p |- ( ph -> .* = ( *r ` R ) ) $=
       ( cedring cfv cnx cstv cop cvv wcel eqid csts wceq fvex chg fvexi starvid
-      co setsid mp2an csca hlhilsca eqtr4di fveq2d syl5eq ) AEGFMNZNZOPNEQUAUGZ
+      co setsid mp2an csca hlhilsca eqtr4di fveq2d eqtrid ) AEGFMNZNZOPNEQUAUGZ
       PNZBPNUPRSERSEURUBGUOUCEGFUDNKUEREPRUPUFUHUIAUQBPAUQCUJNBAUQCUPEDFGHILUPT
       KUQTUKJULUMUN $.
   $}
@@ -646972,7 +646972,7 @@ fixed reference functional determined by this vector (corresponding to
          by NM, 22-Jun-2015.)  (Revised by Mario Carneiro, 29-Jun-2015.) $)
       hlhil0 $p |- ( ph -> .0. = ( 0g ` U ) ) $=
         ( vx vy c0g cfv eqid cv wcel cplusg eqidd hlhilbase wa hlhilplus oveqdr
-        cbs grpidpropd syl5eq ) AGEOPBOPLAMNEUFPZEBAUIUAABCDEUIFHJKIUIQUBAMRUIS
+        cbs grpidpropd eqtrid ) AGEOPBOPLAMNEUFPZEBAUIUAABCDEUIFHJKIUIQUBAMRUIS
         NRUISUCMNETPZBTPAUJBCDEFHJKIUJQUDUEUGUH $.
     $}
 
@@ -646983,7 +646983,7 @@ fixed reference functional determined by this vector (corresponding to
          29-Jun-2015.) $)
       hlhillsm $p |- ( ph -> .(+) = ( LSSum ` U ) ) $=
         ( vx vy clsm cfv cvv eqid cv wcel cbs hlhilbase cplusg hlhilplus oveqdr
-        eqidd wa cdvh fvexi a1i chlh lsmpropd syl5eq ) ABFOPCOPLAMNFUAPZFCQQAUN
+        eqidd wa cdvh fvexi a1i chlh lsmpropd eqtrid ) ABFOPCOPLAMNFUAPZFCQQAUN
         UFACDEFUNGHJKIUNRUBAMSUNTNSUNTUGMNFUCPZCUCPAUOCDEFGHJKIUORUDUEFQTAFGEUH
         PIUIUJCQTACGEUKPJUIUJULUM $.
     $}
@@ -647951,7 +647951,7 @@ fixed reference functional determined by this vector (corresponding to
       1cnd nnnn0d nn0sub syl2anc mpbid binom 3com23 3expia syl5 imp w3a elfzelz
       eqtr3d nnzd zsubcl sylan 1exp syl 3adant2 3ad2ant2 elfznn0 3ad2ant3 expcl
       sylan2 mulid2d eqtrd mulm1 eqtr4d neg1cn mulexp mp3an1 oveq2d bccl syl2an
-      3adant1 nn0cnd sylancr mulassd mulcomd 3expa sumeq2dv itgeq2dv syl5eq ) A
+      3adant1 nn0cnd sylancr mulassd mulcomd 3expa sumeq2dv itgeq2dv eqtrid ) A
       DBUAKUBLZBUHZEKMLNLZKXFMLZFEMLZNLZOLZUCBXEXGUAXIUDLZKUEZCUHZNLZXIXNUFLZOL
       ZXFXNNLZOLZCUGZOLZUCGABXEXKYAAXFXEPZUIXJXTXGOYBAXFQPZXJXTRXFUJAYCUIZXJXLX
       PKXIXNMLZNLZXFUEZXNNLZOLZOLZCUGZXTYDKYGUKLZXINLZXJYKYCYMXJRAYCYLXHXINKQPZ
@@ -648249,7 +648249,7 @@ fixed reference functional determined by this vector (corresponding to
                            _d t
                          = ( 1 / ( 1 x. ( N _C 1 ) ) ) ) $=
       ( vx vy cc0 c1 co cmin cexp cmul wcel cc wceq syl adantr eqtrd cmpt a1i
-      cicc cv citg cdiv elunitcn wa 1m1e0 oveq2i simpr exp0d syl5eq oveq1d 1cnd
+      cicc cv citg cdiv elunitcn wa 1m1e0 oveq2i simpr exp0d eqtrid oveq1d 1cnd
       cbc subcld cn0 cn nnm1nn0 expcld mulid2d sylan2 itgeq2dv cioo 0red itgioo
       1red cfv eqidd oveq2 adantl adantlr cr elioore recn 3syl fvmptd cneg wral
       cdv cpr cnelprrecn nnnn0 nn0cnd mulcld negcld 0cnd dvmptc dvmptsub df-neg
@@ -648312,7 +648312,7 @@ fixed reference functional determined by this vector (corresponding to
       ( c1 co cmin cexp cmul cbc cdiv wceq oveq2d oveq2 oveq12d vi vm cicc citg
       cc0 cv cz wcel cle wbr w3a nnzd cn nnge1 3jca caddc oveq1 adantr itgeq2dv
       syl id eqeq12d lcmineqlem12 wa elnnz1 biimpri 3adant3 adantl lcmineqlem10
-      simpr3 3ad2ant3 eqtrd lcmineqlem11 eqtr4d 1zzd nnge1d fzindd mpdan syl5eq
+      simpr3 3ad2ant3 eqtrd lcmineqlem11 eqtr4d 1zzd nnge1d fzindd mpdan eqtrid
       clt ) ACBUEJUCKZBUFZDJLKZMKZJWBLKZEDLKZMKZNKZUDZJDEDOKZNKZPKZFADUGUHZJDUI
       UJZDEUIUJZUKWIWLQZAWMWNWOADGULADUMUHWNGDUNUTIUOABWAWBUAUFZJLKZMKZWEEWQLKZ
       MKZNKZUDZJWQEWQOKZNKZPKZQBWAWBJJLKZMKZWEEJLKZMKZNKZUDZJJEJOKZNKZPKZQBWAWB
@@ -649312,7 +649312,7 @@ fixed reference functional determined by this vector (corresponding to
       recnd addcld gt0ne0d logcld loggt0b ax-mp mpbir mulne0d redivcld 5re 4nn0
       gtned rpre rpgt0 rpne0d rpne0 expcld cmpt eqid dvrelog2b cdv oveq2d oveq1
       cn dvmptco dvmptadd cpnf mpteq1d eqtrd cnelprrecn 5cn ltled 5nn mpteq2dva
-      dvexp 5m1e4 syl5eq crn ctg ccnfld dvmptc ioossre tgioo2 iooretop dvmptres
+      dvexp 5m1e4 eqtrid crn ctg ccnfld dvmptc ioossre tgioo2 iooretop dvmptres
       ctopn wss dfrp2 pnfxr leidd 0lepnf eqcomd oveq2 dvmptcmul resqcld expne0d
       sqcld 2m1e1 1nn0 eqeltri 2nn dvrelogpow2b ) ABIIIBUGZUCJZKUDJZLUEJZUCJZMJ
       ILUVQIUFUHZMJZUIJZKUVOUJUDJZMJZLUVNUVSMJZUIJZMJZNUEJZMJZMJUVOIUDJZIUVSIUD