rmv ax-5 from moimi + rename prospective space definitions (#3166)

* moimi w/o ax-5

* rename projective space definitions

* operatorname around PrjSp + rewrap

Author: icecream17

discouraged

@@ -16580,6 +16580,7 @@ New usage of "mobidvOLDOLD" is discouraged (0 uses).
 New usage of "moeqOLD" is discouraged (0 uses).
 New usage of "moeuOLD" is discouraged (0 uses).
 New usage of "mofOLD" is discouraged (0 uses).
+New usage of "moimiOLD" is discouraged (0 uses).
 New usage of "mptssALT" is discouraged (0 uses).
 New usage of "mpv" is discouraged (1 uses).
 New usage of "mulassnq" is discouraged (10 uses).
@@ -19425,6 +19426,7 @@ Proof modification of "mobidvOLDOLD" is discouraged (46 steps).
 Proof modification of "moeqOLD" is discouraged (29 steps).
 Proof modification of "moeuOLD" is discouraged (52 steps).
 Proof modification of "mofOLD" is discouraged (62 steps).
+Proof modification of "moimiOLD" is discouraged (17 steps).
 Proof modification of "mptssALT" is discouraged (57 steps).
 Proof modification of "n0lpligALT" is discouraged (74 steps).
 Proof modification of "n2dvds1OLD" is discouraged (37 steps).

set.mm

@@ -21848,10 +21848,22 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
   $}
 
   ${
+    $d x y $.  $d y ph $.  $d y ps $.
     moimi.1 $e |- ( ph -> ps ) $.
     $( The at-most-one quantifier reverses implication.  (Contributed by NM,
-       15-Feb-2006.) $)
+       15-Feb-2006.)  Remove use of ~ ax-5 .  (Revised by Steven Nguyen,
+       9-May-2023.) $)
     moimi $p |- ( E* x ps -> E* x ph ) $=
+      ( vy weq wi wal wex wmo imim1i alimi eximi df-mo 3imtr4i ) BCEFZGZCHZEIAP
+      GZCHZEIBCJACJRTEQSCABPDKLMBCENACENO $.
+  $}
+
+  ${
+    moimiOLD.1 $e |- ( ph -> ps ) $.
+    $( Obsolete version of ~ moimi as of 9-May-2023.  The at-most-one
+       quantifier reverses implication.  (Contributed by NM, 15-Feb-2006.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    moimiOLD $p |- ( E* x ps -> E* x ph ) $=
       ( wi wmo moim mpg ) ABEBCFACFECABCGDH $.
   $}
 
@@ -437024,16 +437036,15 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
     "<IMG SRC='bbr.gif' WIDTH=9 HEIGHT=14 ALT='RR' TITLE='RR'></SUB>&#x200A;";
   althtmldef "-R" as " &minus;<SUB>&#8477;</SUB> ";
   latexdef "-R" as "-\mathbb{R}";
-htmldef "PrjSp1" as
-    "<IMG SRC='bbp.gif' WIDTH=11 HEIGHT=19 ALT=' PrjSp' TITLE='PrjSp'>" +
-    "<SUB>1</SUB>";
-  althtmldef "PrjSp1" as "&#8473;<SUB>1</SUB>";
-  latexdef "PrjSp1" as "\mathbb{P}_1";
 htmldef "PrjSp" as
-    "<IMG SRC='bbp.gif' WIDTH=11 HEIGHT=19 ALT=' PrjSp' TITLE='PrjSp'>" +
-    "<SUB>&#x1D45B;</SUB>";
-  althtmldef "PrjSp" as "&#8473;<SUB>&#x1D45B;</SUB>";
-  latexdef "PrjSp" as "\mathbb{P}_n";
+    "<IMG SRC='bbp.gif' WIDTH=11 HEIGHT=19 ALT=' P' TITLE='P'>roj";
+  althtmldef "PrjSp" as "&#8473;&#x1D563;&#x1D560;&#x1D55B;";
+  latexdef "PrjSp" as "\operatorname{\mathbb{P}\mathrm{roj}}";
+htmldef "PrjSpn" as
+    "<IMG SRC='bbp.gif' WIDTH=11 HEIGHT=19 ALT=' P' TITLE='P'>roj" +
+    "<SUB>n</SUB>";
+  althtmldef "PrjSpn" as "&#8473;&#x1D563;&#x1D560;&#x1D55B;<SUB>n</SUB>";
+  latexdef "PrjSpn" as "\operatorname{\mathbb{P}\mathrm{roj}_\mathrm{n}}";
 /* End of Steven Nguyen's mathbox */
 
 /* Mathbox of Stefan O'Rear */
@@ -616217,156 +616228,156 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 $)
 
-  $c PrjSp1 $.
+  $c PrjSp $.
 
   $( Extend class notation with the projective space function. $)
-  cprjsp1 $a class PrjSp1 $.
+  cprjsp $a class PrjSp $.
 
   ${
     $d v b s x y l $.
     $( Define the projective space function.  (Contributed by BJ and Steven
        Nguyen, 29-Apr-2023.) $)
-    df-prjsp1 $a |- PrjSp1 = ( v e. LVec |-> [_ ( Base ` v ) / b ]_ (
+    df-prjsp $a |- PrjSp = ( v e. LVec |-> [_ ( Base ` v ) / b ]_ (
       ( b \ { ( 0g ` v ) } ) /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\
         E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) ) $.
   $}
 
   ${
     $d b l v x y V $.  $d b v B $.  $d b v .0. $.  $d b v .x. $.  $d b v K $.
-    prjsp1val.b $e |- B = ( Base ` V ) $.
-    prjsp1val.0 $e |- .0. = ( 0g ` V ) $.
-    prjsp1val.x $e |- .x. = ( .s ` V ) $.
-    prjsp1val.s $e |- S = ( Scalar ` V ) $.
-    prjsp1val.k $e |- K = ( Base ` S ) $.
+    prjspval.b $e |- B = ( Base ` V ) $.
+    prjspval.0 $e |- .0. = ( 0g ` V ) $.
+    prjspval.x $e |- .x. = ( .s ` V ) $.
+    prjspval.s $e |- S = ( Scalar ` V ) $.
+    prjspval.k $e |- K = ( Base ` S ) $.
     $( Value of the projective space function.  (Contributed by Steven Nguyen,
        29-Apr-2023.) $)
-    prjsp1val $p |- ( V e. LVec -> ( PrjSp1 ` V ) = ( ( B \ { .0. } ) /.
+    prjspval $p |- ( V e. LVec -> ( PrjSp ` V ) = ( ( B \ { .0. } ) /.
       { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
       ) ) $=
       ( vb cv cbs cfv wa wceq vv c0g csn cdif wel cvsca csca wrex copab cqs csb
-      wcel clvec cprjsp1 cvv fvexd fveq2 syl6eqr eqeq2d biimpd imp sneqd adantr
-      co difeq12d wb imdistani eleq2 anbi12d oveqd rexeqbidv bi2anan9r opabbidv
-      fveq2d syl qseq12d csbied df-prjsp1 fvexi difexi qsex fvmpt ) UAGOUAPZQRZ
-      OPZWCUBRZUCZUDZAOUEZBOUEZSZAPZIPZBPZWCUFRZVDZTZIWCUGRZQRZUHZSZABUIZUJZUKC
-      HUCZUDZWLCULZWNCULZSZWLWMWNEVDZTZIFUHZSZABUIZUJZUMUNWCGTZOWDXCXNUOXOWCQUP
-      XOWEWDTZSZWHXEXBXMXQWECWGXDXOXPWECTZXOXPXRXOWDCWEXOWDGQRCWCGQUQJURUSUTZVA
-      XOWGXDTXPXOWFHXOWFGUBRHWCGUBUQKURVBVCVEXQXAXLABXQXOXRSXAXLVFXOXPXRXSVGXRW
-      KXHXOWTXKXRWIXFWJXGWECWLVHWECWNVHVIXOWQXJIWSFXOWSDQRFXOWRDQXOWRGUGRDWCGUG
-      UQMURVNNURXOWPXIWLXOWOEWMWNXOWOGUFREWCGUFUQLURVJUSVKVLVOVMVPVQABUAOIVRXEX
-      MCXDCGQJVSVTWAWB $.
+      co wcel clvec cprjsp cvv fvexd fveq2 syl6eqr eqeq2d biimpd sneqd difeq12d
+      imp adantr wb imdistani eleq2 anbi12d fveq2d rexeqbidv bi2anan9r opabbidv
+      oveqd syl qseq12d csbied df-prjsp fvexi difexi qsex fvmpt ) UAGOUAPZQRZOP
+      ZWCUBRZUCZUDZAOUEZBOUEZSZAPZIPZBPZWCUFRZULZTZIWCUGRZQRZUHZSZABUIZUJZUKCHU
+      CZUDZWLCUMZWNCUMZSZWLWMWNEULZTZIFUHZSZABUIZUJZUNUOWCGTZOWDXCXNUPXOWCQUQXO
+      WEWDTZSZWHXEXBXMXQWECWGXDXOXPWECTZXOXPXRXOWDCWEXOWDGQRCWCGQURJUSUTVAZVDXO
+      WGXDTXPXOWFHXOWFGUBRHWCGUBURKUSVBVEVCXQXAXLABXQXOXRSXAXLVFXOXPXRXSVGXRWKX
+      HXOWTXKXRWIXFWJXGWECWLVHWECWNVHVIXOWQXJIWSFXOWSDQRFXOWRDQXOWRGUGRDWCGUGUR
+      MUSVJNUSXOWPXIWLXOWOEWMWNXOWOGUFREWCGUFURLUSVNUTVKVLVOVMVPVQABUAOIVRXEXMC
+      XDCGQJVSVTWAWB $.
   $}
 
   ${
     $d B x y $.  $d X x y l m $.  $d Y x y l m $.  $d K x y l m $.
     $d .x. x y l m $.
-    prjsp1rel.1 $e |- .~ = { <. x , y >. |
+    prjsprel.1 $e |- .~ = { <. x , y >. |
       ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } $.
-    $( Utility theorem regarding the relation used in ` PrjSp1 ` .
-       (Contributed by Steven Nguyen, 29-Apr-2023.) $)
-    prjsp1rel $p |- ( X .~ Y <->
+    $( Utility theorem regarding the relation used in ` PrjSp ` .  (Contributed
+       by Steven Nguyen, 29-Apr-2023.) $)
+    prjsprel $p |- ( X .~ Y <->
       ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) ) $=
       ( cv co wceq wrex wa weq simpll simpr simplr oveq12d eqeq12d cbvrexdva
       brabg2a ) ALZJLZBLZEMZNZJGOHFLZIEMZNZFGOABHICCDUEHNZUGINZPZUIULJFGUOJFQZP
       ZUEHUHUKUMUNUPRUQUFUJUGIEUOUPSUMUNUPTUAUBUCKUD $.
 
     $d Z l m n o x y $.  $d V m n o $.  $d X n o $.  $d Y n o $.  $d K n o $.
     $d .x. n o $.  $d S o $.  $d .~ m n o $.
-    prjsp1ertr.b $e |- B = ( Base ` V ) $.
-    prjsp1ertr.s $e |- S = ( Scalar ` V ) $.
-    prjsp1ertr.x $e |- .x. = ( .s ` V ) $.
-    prjsp1ertr.k $e |- K = ( Base ` S ) $.
-    $( The relation in ` PrjSp1 ` is transitive.  (Contributed by Steven
-       Nguyen, 1-May-2023.) $)
-    prjsp1ertr $p |- ( ( V e. LVec /\ ( X .~ Y /\ Y .~ Z ) ) -> X .~ Z ) $=
-      ( wcel wa co vm vn vo clvec wbr cv wceq prjsp1rel simprbi ad2antrl adantl
-      wrex ad3antlr simplrl ad3antrrr simpll sylbi syl simplrr simplr cmulr cfv
-      crg clmod lveclmod lmodring ad5antr simp-4r eqid ringcl syl3anc wb eqeq2d
-      oveq1 simpr oveq2d simpllr lmodvsass syl13anc 3eqtr4d rspcedvd syl21anbrc
-      ex rexlimdva mpd ) HUDRZIJDUEZJKDUEZSZSZIUAUFZJFTZUGZUAGULZIKDUEZWGWNWFWH
-      WGICRZJCRZSZWNABCDFUAGIJLMUHZUIUJWJWMWOUAGWJWKGRZSZWMWOXAWMSZJUBUFZKFTZUG
-      ZUBGULZWOWIXFWFWTWMWHXFWGWHWQKCRZSZXFABCDFUBGJKLMUHZUIUKUMXBXEWOUBGXBXCGR
-      ZSZXEWOXKXESZWPXGIUCUFZKFTZUGZUCGULWOXLWGWPXAWGWMXJXEWFWGWHWTUNUOWGWRWNSW
-      PWSWPWQWNUPUQURXLWHXGXAWHWMXJXEWFWGWHWTUSUOWHXHXFSXGXIWQXGXFUTUQURZXLXOIW
-      KXCEVAVBZTZKFTZUGZUCXRGXLEVCRZWTXJXRGRWFYAWIWTWMXJXEWFHVDRZYAHVEZEHOVFURV
-      GWJWTWMXJXEVHZXBXJXEUTZGEXQWKXCQXQVIZVJVKXMXRUGZXOXTVLXLYGXNXSIXMXRKFVNVM
-      UKXLWLWKXDFTZIXSXLJXDWKFXKXEVOVPXAWMXJXEVQXLYBWTXJXGXSYHUGWFYBWIWTWMXJXEY
-      CVGYDYEXPWKXCFXQEGCHKNOPQYFVRVSVTWAABCDFUCGIKLMUHWBWCWDWEWCWDWE $.
+    prjspertr.b $e |- B = ( Base ` V ) $.
+    prjspertr.s $e |- S = ( Scalar ` V ) $.
+    prjspertr.x $e |- .x. = ( .s ` V ) $.
+    prjspertr.k $e |- K = ( Base ` S ) $.
+    $( The relation in ` PrjSp ` is transitive.  (Contributed by Steven Nguyen,
+       1-May-2023.) $)
+    prjspertr $p |- ( ( V e. LVec /\ ( X .~ Y /\ Y .~ Z ) ) -> X .~ Z ) $=
+      ( wcel wa co vm vn vo clvec cv wceq wrex prjsprel simprbi ad2antrl adantl
+      wbr simplrl ad3antrrr simpll sylbi syl simplrr simplr cmulr cfv crg clmod
+      ad3antlr lveclmod lmodring ad5antr simp-4r ringcl syl3anc wb oveq1 eqeq2d
+      eqid simpr oveq2d simpllr lmodvsass syl13anc 3eqtr4d syl21anbrc rexlimdva
+      rspcedvd ex mpd ) HUDRZIJDULZJKDULZSZSZIUAUEZJFTZUFZUAGUGZIKDULZWGWNWFWHW
+      GICRZJCRZSZWNABCDFUAGIJLMUHZUIUJWJWMWOUAGWJWKGRZSZWMWOXAWMSZJUBUEZKFTZUFZ
+      UBGUGZWOWIXFWFWTWMWHXFWGWHWQKCRZSZXFABCDFUBGJKLMUHZUIUKVDXBXEWOUBGXBXCGRZ
+      SZXEWOXKXESZWPXGIUCUEZKFTZUFZUCGUGWOXLWGWPXAWGWMXJXEWFWGWHWTUMUNWGWRWNSWP
+      WSWPWQWNUOUPUQXLWHXGXAWHWMXJXEWFWGWHWTURUNWHXHXFSXGXIWQXGXFUSUPUQZXLXOIWK
+      XCEUTVAZTZKFTZUFZUCXRGXLEVBRZWTXJXRGRWFYAWIWTWMXJXEWFHVCRZYAHVEZEHOVFUQVG
+      WJWTWMXJXEVHZXBXJXEUSZGEXQWKXCQXQVNZVIVJXMXRUFZXOXTVKXLYGXNXSIXMXRKFVLVMU
+      KXLWLWKXDFTZIXSXLJXDWKFXKXEVOVPXAWMXJXEVQXLYBWTXJXGXSYHUFWFYBWIWTWMXJXEYC
+      VGYDYEXPWKXCFXQEGCHKNOPQYFVRVSVTWCABCDFUCGIKLMUHWAWDWBWEWDWBWE $.
 
     $d B m $.  $d S m $.
-    $( The relation in ` PrjSp1 ` is reflexive.  (Contributed by Steven Nguyen,
+    $( The relation in ` PrjSp ` is reflexive.  (Contributed by Steven Nguyen,
        30-Apr-2023.) $)
-    prjsp1erref $p |- ( V e. LVec -> ( X e. B <-> X .~ X ) ) $=
+    prjsperref $p |- ( V e. LVec -> ( X e. B <-> X .~ X ) ) $=
       ( vm wcel wa co wceq clvec cv wrex wbr cur cfv clmod lveclmod adantr eqid
       lmod1cl syl simpr oveq1d eqeq2d lmodvs1 eqcomd rspcedvd ex pm4.71d pm4.24
-      sylan anbi1i syl6bb prjsp1rel syl6bbr ) HUAQZICQZVHVHRZIPUBZIFSZTZPGUCZRZ
-      IIDUDVGVHVHVMRVNVGVHVMVGVHVMVGVHRZVLIEUEUFZIFSZTPVPGVOHUGQZVPGQVGVRVHHUHZ
-      UIVPEGHMOVPUJZUKULVOVJVPTZRZVKVQIWBVJVPIFVOWAUMUNUOVOVQIVGVRVHVQITVSFVPEC
-      HILMNVTUPVBUQURUSUTVHVIVMVHVAVCVDABCDFPGIIJKVEVF $.
+      sylan anbi1i syl6bb prjsprel syl6bbr ) HUAQZICQZVHVHRZIPUBZIFSZTZPGUCZRZI
+      IDUDVGVHVHVMRVNVGVHVMVGVHVMVGVHRZVLIEUEUFZIFSZTPVPGVOHUGQZVPGQVGVRVHHUHZU
+      IVPEGHMOVPUJZUKULVOVJVPTZRZVKVQIWBVJVPIFVOWAUMUNUOVOVQIVGVRVHVQITVSFVPECH
+      ILMNVTUPVBUQURUSUTVHVIVMVHVAVCVDABCDFPGIIJKVEVF $.
 
     $d .x. n $.  $d K n $.  $d Y n $.  $d .0. n $.  $d .0. m $.  $d B n $.
     $d S n $.
-    prjsp1ersym.1 $e |- .0. = ( 0g ` V ) $.
-    $( The relation in ` PrjSp1 ` is symmetric.  (Contributed by Steven Nguyen,
+    prjspersym.1 $e |- .0. = ( 0g ` V ) $.
+    $( The relation in ` PrjSp ` is symmetric.  (Contributed by Steven Nguyen,
        1-May-2023.) $)
-    prjsp1ersym $p |- ( ( V e. LVec /\ X .~ Y /\ X =/= .0. ) -> Y .~ X ) $=
-      ( wcel wceq vm vn clvec wbr wne w3a cv co wa wrex prjsp1rel pm3.22 adantr
-      simpll2 sylbi syl cinvr cfv cdr c0g simpll1 lvecdrng simplr simpll3 simpr
-      neneqd oveq1d clmod lveclmod simpld eqid lmod0vs syl2anc mtand drnginvrcl
-      3eqtrd neqned syl3anc wb oveq1 eqeq2d adantl csn wn eldifd simprd lvecinv
-      nelsn mpbid rspcedvd sylanbrc 3ad2ant2 r19.29a ) HUCSZIJDUDZIKUEZUFZIUAUG
-      ZJFUHZTZJIDUDZUAGWQWRGSZUIZWTUIZJCSZICSZUIZJUBUGZIFUHZTZUBGUJXAXDWOXGWNWO
-      WPXBWTUNWOXFXEUIZWTUAGUJZUIZXGABCDFUAGIJLMUKZXKXGXLXFXEULUMUOUPZXDXJJWREU
-      QURZURZIFUHZTZUBXQGXDEUSSZXBWREUTURZUEZXQGSXDWNXTWNWOWPXBWTVAZEHOVBUPWQXB
-      WTVCZXDWRYAXDWRYATZIKTXDIKWNWOWPXBWTVDVFXDYEUIZIWSYAJFUHZKXCWTYEVCYFWRYAJ
-      FXDYEVEVGYFHVHSZXEYGKTYFWNYHXDWNYEYCUMHVIUPXDXEYEXDXEXFXOVJZUMFEYACHJKNOP
-      YAVKZRVLVMVPVNVQZGEXPWRYAQYJXPVKZVOVRXHXQTZXJXSVSXDYMXIXRJXHXQIFVTWAWBXDW
-      TXSXCWTVEXDWRFEXPGCHIJYANPOQYJYLYCXDWRGYAWCZYDXDYBWRYNSWDYKWRYAWHUPWEXDXE
-      XFXOWFYIWGWIWJABCDFUBGJILMUKWKWOWNXLWPWOXMXLXNXKXLVEUOWLWM $.
+    prjspersym $p |- ( ( V e. LVec /\ X .~ Y /\ X =/= .0. ) -> Y .~ X ) $=
+      ( wcel wceq vm vn clvec wbr wne w3a cv co wa wrex simpll2 prjsprel pm3.22
+      adantr sylbi syl cinvr cfv cdr c0g simpll1 lvecdrng simplr simpll3 neneqd
+      simpr oveq1d clmod lveclmod simpld eqid lmod0vs syl2anc 3eqtrd drnginvrcl
+      mtand neqned syl3anc wb oveq1 eqeq2d adantl csn nelsn eldifd simprd mpbid
+      wn lvecinv rspcedvd sylanbrc 3ad2ant2 r19.29a ) HUCSZIJDUDZIKUEZUFZIUAUGZ
+      JFUHZTZJIDUDZUAGWQWRGSZUIZWTUIZJCSZICSZUIZJUBUGZIFUHZTZUBGUJXAXDWOXGWNWOW
+      PXBWTUKWOXFXEUIZWTUAGUJZUIZXGABCDFUAGIJLMULZXKXGXLXFXEUMUNUOUPZXDXJJWREUQ
+      URZURZIFUHZTZUBXQGXDEUSSZXBWREUTURZUEZXQGSXDWNXTWNWOWPXBWTVAZEHOVBUPWQXBW
+      TVCZXDWRYAXDWRYATZIKTXDIKWNWOWPXBWTVDVEXDYEUIZIWSYAJFUHZKXCWTYEVCYFWRYAJF
+      XDYEVFVGYFHVHSZXEYGKTYFWNYHXDWNYEYCUNHVIUPXDXEYEXDXEXFXOVJZUNFEYACHJKNOPY
+      AVKZRVLVMVNVPVQZGEXPWRYAQYJXPVKZVOVRXHXQTZXJXSVSXDYMXIXRJXHXQIFVTWAWBXDWT
+      XSXCWTVFXDWRFEXPGCHIJYANPOQYJYLYCXDWRGYAWCZYDXDYBWRYNSWHYKWRYAWDUPWEXDXEX
+      FXOWFYIWIWGWJABCDFUBGJILMULWKWOWNXLWPWOXMXLXNXKXLVFUOWLWM $.
 
     $d V a b c $.  $d .0. a b c $.  $d B a b c $.  $d .~ a b c $.  $d R c $.
     $d a b c l x y $.
-    $( The relation in ` PrjSp1 ` is an equivalence relation.  (Contributed by
+    $( The relation in ` PrjSp ` is an equivalence relation.  (Contributed by
        Steven Nguyen, 1-May-2023.) $)
-    prjsp1er $p |- ( V e. LVec ->
+    prjsper $p |- ( V e. LVec ->
       ( .~ i^i ( ( B \ { .0. } ) X. ( B \ { .0. } ) ) ) Er ( B \ { .0. } ) ) $=
       ( wcel wbr wa brinxp2 va vb vc clvec csn cdif cxp cin wrel relinxp a1i cv
-      simprl ancomd simpl simprr eldifsni simpl2im prjsp1ersym syl3anc sylanbrc
-      sylan2b anbi12i simp-4l ancoms simprlr anasss simprrr prjsp1ertr syl12anc
-      syl21anbrc eldifi prjsp1erref syl5ib pm4.71d anidm anbi1i syl6bbr iserd
-      wne ) HUDQZUAUBUCCIUEZUFZDWCWCUGUHZWDUIWAWCWCDUJUKUAULZUBULZWDRZWAWEWCQZW
-      FWCQZSZWEWFDRZSZWFWEWDRZWCWCWEWFDTZWAWLSZWIWHSWFWEDRZWMWOWHWIWAWJWKUMUNZW
-      OWAWKWEIVTZWPWAWLUOWAWJWKUPWOWIWHWRWQWECIUQURABCDEFGHWEWFIJKLMNOPUSUTWCWC
-      WFWEDTVAVBWGWFUCULZWDRZSWAWLWIWSWCQZSZWFWSDRZSZSZWEWSWDRZWGWLWTXDWNWCWCWF
-      WSDTVCWAXESZWHXAWEWSDRZXFXEWAWHWHWIWKXDWAVDVEWAWLXDXAWOWIXAXCVFVGXGWAWKXC
-      XHWAXEUOWAWJWKXDVFWAWLXBXCVHABCDEFGHWEWFWSJKLMNOVIVJWCWCWEWSDTVKVBWAWHWHW
-      HSZWEWEDRZSZWEWEWDRWAWHWHXJSXKWAWHXJWHWECQWAXJWECWBVLABCDEFGHWEJKLMNOVMVN
-      VOXIWHXJWHVPVQVRWCWCWEWEDTVRVS $.
+      simprl ancomd wne simpl simprr eldifsni simpl2im syl3anc sylanbrc sylan2b
+      prjspersym anbi12i simp-4l ancoms simprlr anasss simprrr prjspertr eldifi
+      syl12anc syl21anbrc prjsperref syl5ib pm4.71d anidm anbi1i syl6bbr iserd
+      ) HUDQZUAUBUCCIUEZUFZDWCWCUGUHZWDUIWAWCWCDUJUKUAULZUBULZWDRZWAWEWCQZWFWCQ
+      ZSZWEWFDRZSZWFWEWDRZWCWCWEWFDTZWAWLSZWIWHSWFWEDRZWMWOWHWIWAWJWKUMUNZWOWAW
+      KWEIUOZWPWAWLUPWAWJWKUQWOWIWHWRWQWECIURUSABCDEFGHWEWFIJKLMNOPVCUTWCWCWFWE
+      DTVAVBWGWFUCULZWDRZSWAWLWIWSWCQZSZWFWSDRZSZSZWEWSWDRZWGWLWTXDWNWCWCWFWSDT
+      VDWAXESZWHXAWEWSDRZXFXEWAWHWHWIWKXDWAVEVFWAWLXDXAWOWIXAXCVGVHXGWAWKXCXHWA
+      XEUPWAWJWKXDVGWAWLXBXCVIABCDEFGHWEWFWSJKLMNOVJVLWCWCWEWSDTVMVBWAWHWHWHSZW
+      EWEDRZSZWEWEWDRWAWHWHXJSXKWAWHXJWHWECQWAXJWECWBVKABCDEFGHWEJKLMNOVNVOVPXI
+      WHXJWHVQVRVSWCWCWEWEDTVSVT $.
   $}
 
-  $c PrjSp $.
+  $c PrjSpn $.
 
   $( Extend class notation with the n-dimensional projective space function. $)
-  cprjsp $a class PrjSp $.
+  cprjspn $a class PrjSpn $.
 
   ${
     $d n k $.
     $( Define the n-dimensional projective space function.  A projective space
        of dimension 1 is a projective line, and a projective space of dimension
        2 is a projective plane.  Compare ~ df-ehl .  (Contributed by BJ and
        Steven Nguyen, 29-Apr-2023.) $)
-    df-prjsp $a |- PrjSp = ( n e. NN0 , k e. DivRing |->
-      ( PrjSp1 ` ( k freeLMod ( 1 ... n ) ) ) ) $.
+    df-prjspn $a |- PrjSpn = ( n e. NN0 , k e. DivRing |->
+      ( PrjSp ` ( k freeLMod ( 1 ... n ) ) ) ) $.
   $}
 
   ${
     $d n k N $.  $d n k K $.
     $( Value of the n-dimensional projective space function.  (Contributed by
        Steven Nguyen, 1-May-2023.) $)
-    prjspval $p |- ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSp K ) =
-      ( PrjSp1 ` ( K freeLMod ( 1 ... N ) ) ) ) $=
-      ( vn vk cn0 cdr cv c1 cfz co cfrlm cprjsp1 cfv cprjsp oveq2 oveq2d fveq2d
-      wceq fvoveq1 df-prjsp fvex ovmpt2 ) CDBAEFDGZHCGZIJZKJZLMAHBIJZKJZLMNUCUG
-      KJZLMUDBRZUFUILUJUEUGUCKUDBHIOPQUCAUGLKSDCTUHLUAUB $.
+    prjspnval $p |- ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) =
+      ( PrjSp ` ( K freeLMod ( 1 ... N ) ) ) ) $=
+      ( vn vk cn0 cdr cv c1 cfz co cfrlm cprjsp cfv cprjspn oveq2 oveq2d fveq2d
+      wceq fvoveq1 df-prjspn fvex ovmpt2 ) CDBAEFDGZHCGZIJZKJZLMAHBIJZKJZLMNUCU
+      GKJZLMUDBRZUFUILUJUEUGUCKUDBHIOPQUCAUGLKSDCTUHLUAUB $.
   $}
 
   ${