diff --git a/changes-set.txt b/changes-set.txt index c6842ac6dd..16ce5a1330 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -93,6 +93,11 @@ make a github issue.) DONE: Date Old New Notes 17-Oct-25 decexp2 --- deleted - unused +13-Oct-25 ssinss1d [same] Moved from GS's mathbox to main set.mm +13-Oct-25 opeliun2xp [same] Moved from AV's mathbox to main set.mm +13-Oct-25 fvelima2 [same] Moved from GS's mathbox to main set.mm +13-Oct-25 pwssfi [same] Moved from GS's mathbox to main set.mm +13-Oct-25 pnfged [same] Moved from GS's mathbox to main set.mm 7-Oct-25 tgioo4 [same] Moved from GS's mathbox to main set.mm 6-Oct-25 nel2nelin [same] Moved from GS's mathbox to main set.mm 6-Oct-25 nel1nelin [same] Moved from GS's mathbox to main set.mm diff --git a/set.mm b/set.mm index 106ebbc1eb..f7ae9624eb 100644 --- a/set.mm +++ b/set.mm @@ -40555,6 +40555,14 @@ many things are technically classes despite morally (and provably) being ssinss1 $p |- ( A C_ C -> ( A i^i B ) C_ C ) $= ( cin wss wi inss1 sstr2 ax-mp ) ABDZAEACEJCEFABGJACHI $. + ${ + ssinss1d.1 $e |- ( ph -> A C_ C ) $. + $( Intersection preserves subclass relationship. (Contributed by Glauco + Siliprandi, 17-Aug-2020.) $) + ssinss1d $p |- ( ph -> ( A i^i B ) C_ C ) $= + ( wss cin ssinss1 syl ) ABDFBCGDFEBCDHI $. + $} + $( Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.) $) inss $p |- ( ( A C_ C \/ B C_ C ) -> ( A i^i B ) C_ C ) $= @@ -55587,6 +55595,26 @@ of the restricted converse (see ~ cnvrescnv ). (Contributed by NM, VNRS $. $} + ${ + $d x z A $. $d x z B $. $d x z C $. $d x y z $. + $( Membership of an ordered pair in a union of Cartesian products over its + second component, analogous to ~ opeliunxp . (Contributed by AV, + 30-Mar-2019.) $) + opeliun2xp $p |- ( <. C , y >. e. U_ y e. B ( A X. { y } ) <-> + ( y e. B /\ C e. A ) ) $= + ( vx vz cv cop csn cxp wcel wa wex weq eleq2d anbi12d bitri anbi2i 3bitri + wceq ciun wrex cab wsb csb df-iun eleq2i opex nfv nfs1v nfcsb1v nfcv nfxp + df-rex nfcri nfan sbequ12 csbeq1a sneq xpeq12d eleq1 anbi2d exbidv bitrid + cbvexv1 elab opelxp an13 ancom velsn equcom anbi1i exbii sbequ12r equcoms + eqcomd equsexvw ) DAGZHZACBVRIZJZUAZKVSEGZWAKZACUBZEUCZKVRCKZAFUDZVSAFGZB + UEZWIIZJZKZLZFMZWGDBKZLZWBWFVSAECWAUFUGWEWOEVSDVRUHWEWHWCWLKZLZFMZWCVSTZW + OWEWGWDLZAMWTWDACUNXBWSAFXBFUIWHWRAWGAFUJAEWLAWJWKAWIBUKAWKULUMUOUPAFNZWG + WHWDWRWGAFUQXCWAWLWCXCBWJVTWKAWIBURZVRWIUSUTOPVEQXAWSWNFXAWRWMWHWCVSWLVAV + BVCVDVFWOFANZWHDWJKZLZLZFMWQWNXHFWNWHXFVRWKKZLZLZXIXGLZXHWMXJWHDVRWJWKVGR + XKXIXFWHLZLXLWHXFXIVHXMXGXIXFWHVIRQXIXEXGXIXCXEAWIVJAFVKQVLSVMXGWQFAXEWHW + GXFWPWGFAVNXEWJBDXEBWJBWJTAFXDVOVPOPVQQS $. + $} + ${ $d x y A $. $d x y B $. $d x y C $. $( Distributive law for Cartesian product over union. Theorem 103 of @@ -66483,6 +66511,20 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). ( wfn wcel wa cfv wceq wbr cop fnbrfvb df-br bitrdi ) DAEBAFGBDHCIBCDJBCKDF ABCDLBCDMN $. + ${ + $d A x $. $d B x $. $d C x $. $d F x $. + $( Function value in an image. (Contributed by Glauco Siliprandi, + 2-Jan-2022.) $) + fvelima2 $p |- ( ( F Fn A /\ B e. ( F " C ) ) + -> E. x e. ( A i^i C ) ( F ` x ) = B ) $= + ( cima wcel wfn cv wbr wa wex cfv wceq cin wrex elimag df-rex adantrl imp + ibi sylib fnbr simprl elind wfun fnfun funbrfv sylan jca ex eximdv sylibr + sylan2 ) CEDFZGZEBHZAIZDGZURCEJZKZALZUREMCNZABDOZPZUPUTADPZVBUPVFACEDUOQU + AUTADRUBUQVBKURVDGZVCKZALZVEUQVBVIUQVAVHAUQVAVHUQVAKZVGVCVJBDURUQUTURBGUS + BURCEUCSUQUSUTUDUEUQUTVCUSUQEUFZUTVCBEUGVKUTVCURCEUHTUISUJUKULTVCAVDRUMUN + $. + $} + $( Equivalence of function value and binary relation. (Contributed by NM, 26-Mar-2006.) $) funbrfvb $p |- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> A F B ) ) $= @@ -96891,6 +96933,17 @@ excluded middle (LEM), and in ILE the LEM is not accepted as necessarily $( $j usage 'cnvfi' avoids 'ax-pow'; $) $} + ${ + $d A x $. + $( Every element of the power set of ` A ` is finite if and only if ` A ` + is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $) + pwssfi $p |- ( A e. V -> ( A e. Fin <-> ~P A C_ Fin ) ) $= + ( vx wcel cfn cpw wss wral elpwi ssfi sylan2 ralrimiva dfss3 sylibr pwidg + cv biimpi eleq1 rspcva syl2an ex impbid2 ) ABDZAEDZAFZEGZUDCPZEDZCUEHZUFU + DUHCUEUGUEDUDUGAGUHUGAIAUGJKLCUEEMZNUCUFUDUCAUEDUIUDUFABOUFUIUJQUHUDCAUEU + GAERSTUAUB $. + $} + ${ $d A x y z $. $d F x y z $. $( A version of ~ fnex for finite sets that does not require Replacement or @@ -144890,6 +144943,14 @@ Infinity and the extended real number system (cont.) ( cxr wcel cpnf cle wbr clt wn pnfnlt wb pnfxr xrlenlt mpan2 mpbird ) ABCZA DEFZDAGFHZAIODBCPQJKADLMN $. + ${ + pnfged.1 $e |- ( ph -> A e. RR* ) $. + $( Plus infinity is an upper bound for extended reals. (Contributed by + Glauco Siliprandi, 5-Feb-2022.) $) + pnfged $p |- ( ph -> A <_ +oo ) $= + ( cxr wcel cpnf cle wbr pnfge syl ) ABDEBFGHCBIJ $. + $} + $( An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021.) $) xnn0n0n1ge2b $p |- ( N e. NN0* -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) ) $= @@ -502594,6 +502655,17 @@ and the expression ( x e. A /\ x e. B ) ` . ( cv wcel c0 wne wex n0 sylib exlimddv ) ACGDHZBCADIJOCKECDLMFN $. $} + ${ + $d A x $. $d B x $. $d ph x $. + reu6d.1 $e |- ( ph -> B e. A ) $. + reu6d.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> x = B ) ) $. + $( A condition which implies existential uniqueness. (Contributed by + Thierry Arnoux, 13-Oct-2025.) $) + reu6dv $p |- ( ph -> E! x e. A ps ) $= + ( wcel cv wceq wb wral wreu ralrimiva reu6i syl2anc ) AEDHBCIEJKZCDLBCDMF + AQCDGNBCDEOP $. + $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -503316,6 +503388,21 @@ Class abstractions (a.k.a. class builders) $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Singletons +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + elsnd.1 $e |- ( ph -> A e. { B } ) $. + $( There is at most one element in a singleton. (Contributed by Thierry + Arnoux, 13-Oct-2025.) $) + elsnd $p |- ( ph -> A = B ) $= + ( csn wcel wceq elsni syl ) ABCEFBCGDBCHI $. + $} + + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- Unordered pairs @@ -503754,6 +503841,20 @@ Class abstractions (a.k.a. class builders) CPZAUBCPZOUCDEOZOABUBCQUAUDUEUCAHICDEFGJKRST $. $} + ${ + $d A x y $. $d A x z $. $d B y $. $d B z $. $d C y $. $d E x $. + $d ph x y $. + iunxpssiun1.1 $e |- ( ( ph /\ x e. A ) -> C C_ E ) $. + $( Provide an upper bound for the indexed union of cartesian products. + (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + iunxpssiun1 $p |- ( ph -> U_ x e. A ( B X. C ) C_ ( U_ x e. A B X. E ) ) $= + ( vy cxp ciun cv csb wss wral wcel wa ssiun2 adantl nfcv nfcsb1v sseqtrdi + csbeq1a cbviun xpss12 ralrimiva nfiun nfxp iunssf sylibr xpeq1i sseqtrrdi + syl2anc ) ABCDEIZJZHCBHKZDLZJZFIZBCDJZFIAUMURMZBCNUNURMAUTBCABKCOZPZDUQME + FMUTVBDUSUQVADUSMABCDQRBHCDUPHDSBUODTZBUODUBUCZUAGDUQEFUDULUEBCUMURBUQFHB + CUPBCSVCUFBFSUGUHUIUSUQFVDUJUK $. + $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -504595,6 +504696,21 @@ Class abstractions (a.k.a. class builders) FADLUAADLUBUCUDUKBCLEFGJABDLCPUMUGIKUEUHUI $. $} + ${ + $d A f x $. $d B f x y $. $d ch y $. $d f ph x $. $d f ps $. + ac6mapd.1 $e |- ( y = ( f ` x ) -> ( ps <-> ch ) ) $. + ac6mapd.2 $e |- ( ph -> A e. V ) $. + ac6mapd.3 $e |- ( ph -> B e. W ) $. + ac6mapd.4 $e |- ( ( ph /\ x e. A ) -> E. y e. B ps ) $. + $( Axiom of choice equivalent, deduction form. (Contributed by Thierry + Arnoux, 13-Oct-2025.) $) + ac6mapd $p |- ( ph -> E. f e. ( B ^m A ) A. x e. A ch ) $= + ( cv wcel wral wa wex wrex cmap co wf ralrimiva ac6sg sylc elmapd biimprd + anim1d eximdv mpd df-rex sylibr ) AHOZGFUAUBZPZCDFQZRZHSZUQHUOTAFGUNUCZUQ + RZHSZUSAFIPBEGTZDFQVBLAVCDFNUDBCDEFGHIKUEUFAVAURHAUTUPUQAUPUTAGFUNJIMLUGU + HUIUJUKUQHUOULUM $. + $} + $( Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017.) $) fnresin $p |- ( F Fn A -> ( F |` B ) Fn ( A i^i B ) ) $= @@ -505669,6 +505785,23 @@ its graph has a given second element (that is, function value). $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + The mapping operation +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + elmaprd.1 $e |- ( ph -> A e. V ) $. + elmaprd.2 $e |- ( ph -> B e. W ) $. + elmaprd.3 $e |- ( ph -> F e. ( B ^m A ) ) $. + $( Deduction associated with ~ elmapd . Reverse direction of ~ elmapdd . + (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + elmaprd $p |- ( ph -> F : A --> B ) $= + ( cmap co wcel wf elmapd mpbid ) ADCBJKLBCDMIACBDFEHGNO $. + $} + + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- Support of a function @@ -507985,6 +508118,17 @@ its graph has a given second element (that is, function value). xnn01gt syl bitrd ) ABCZADEFGHZICZJADKZUQCZJZGUSLMZUPURUTUPURANCZUTOZUTNPQR SZDUADNUBURVDTUCNVEDUDNAUQDUEUFUPVCUTABUGUHUIUJUPUSUKCVAVBTABULUSUMUNUO $. + $( The size of a proper subset is less than the size of its finite superset. + (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + hashpss $p |- ( ( A e. Fin /\ B C. A ) -> ( # ` B ) < ( # ` A ) ) $= + ( cfn wcel wa chash cfv cxr cle wbr wne clt cvv simpl simpr hashxrcl adantr + wpss wceq cen pssssd ssexd syl wss hashss syldan ssfid hashen biimpa ensymd + syl21anc fisseneq syl3anc pssned neneqd pm2.65da xrltlen biimpar syl22anc + neqned ) ACDZBARZEZBFGZHDZAFGZHDZVDVFIJZVFVDKZVDVFLJZVCBMDVEVCBACVAVBNZVCBA + VAVBOZUAZUBBMPUCVAVGVBACPQVAVBBAUDZVHVMABCUEUFVCVFVDVCVFVDSZBASZVCVOEZVAVNB + ATJVPVCVAVOVKQZVCVNVOVMQZVQABVQVABCDZVOABTJZVRVQABVRVSUGVCVOOVAVTEVOWAABUHU + IUKUJBAULUMVQBAVQBAVCVBVOVLQUNUOUPUTVEVGEVJVHVIEVDVFUQURUS $. + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -508361,21 +508505,21 @@ its graph has a given second element (that is, function value). nexple $p |- ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) -> A <_ ( B ^ A ) ) $= ( wcel c2 cle wbr cexp co cc0 wceq wa simpr wi c1 id oveq2 breq12d imbi2d a1i letrd vk vn cn0 cr w3a cn simpl2 simpl3 cv caddc simpl 1nn0 1red 1le2 - 2re expge1d cmul nnnn0d nn0red readdcld 3ad2ant2 remulcld reexpcld nnge1d - simp1 leadd2dd recnd times2d breqtrrd nn0ge0d lemul2ad 0red 0le2 lemul1ad - simp2r simp3 expp1d 3exp a2d nnind 3impib syl3anc 0le1 oveq2d exp0d eqtrd - 3brtr4d wo elnn0 biimpi 3ad2ant1 mpjaodan ) AUCCZBUDCZDBEFZUEZAUFCZABAGHZ - EFZAIJZWPWQKWQWNWOWSWPWQLWMWNWOWQUGWMWNWOWQUHWQWNWOWSWNWOKZUAUIZBXBGHZEFZ - MXANBNGHZEFZMXAUBUIZBXGGHZEFZMXAXGNUJHZBXJGHZEFZMXAWSMUAUBAXBNJZXDXFXAXMX - BNXCXEEXMOXBNBGPQRXBXGJZXDXIXAXNXBXGXCXHEXNOXBXGBGPQRXBXJJZXDXLXAXOXBXJXC - XKEXOOXBXJBGPQRXBAJZXDWSXAXPXBAXCWREXPOXBABGPQRXABNWNWOUKZNUCCXAULSXANDBX - AUMDUDCZXAUOSZXQNDEFXAUNSWNWOLZTUPXGUFCZXAXIXLYAXAXIXLYAXAXIUEZXJXHBUQHZX - KEYBXJXGBUQHZYCYBXGNYBXGYBXGYAXAXIVEZURZUSZYBUMZUTZYBXGBYGXAYAWNXIXQVAZVB - ZYBXHBYBBXGYJYFVCZYJVBYBXJXGDUQHZYDYIYBXGDYGXRYBUOSZVBYKYBXJXGXGUJHYMEYBN - XGXGYHYGYGYBXGYEVDVFYBXGYBXGYGVGVHVIYBDBXGYNYJYGYBXGYFVJYAWNWOXIVOVKTYBXG - XHBYGYLYJXAYAIBEFXIXAIDBXAVLXSXQIDEFXAVMSXTTVAYAXAXIVPVNTYBBXGYBBYJVGYFVQ - VIVRVSVTWAWBWPWTKZINAWREINEFYOWCSWPWTLZYOWRBIGHNYOAIBGYPWDYOBYOBWMWNWOWTU - GVGWEWFWGWMWNWQWTWHZWOWMYQAWIWJWKWL $. + 2re expge1d simp1 nnred readdcld 3ad2ant2 remulcld nnnn0d reexpcld nnge1d + cmul leadd2dd times2d breqtrrd nn0ge0d simp2r lemul2ad 0red 0le2 lemul1ad + recnd simp3 expp1d 3exp a2d nnind 3impib syl3anc 0le1 exp0d eqtrd 3brtr4d + oveq2d wo elnn0 biimpi 3ad2ant1 mpjaodan ) AUCCZBUDCZDBEFZUEZAUFCZABAGHZE + FZAIJZWPWQKWQWNWOWSWPWQLWMWNWOWQUGWMWNWOWQUHWQWNWOWSWNWOKZUAUIZBXBGHZEFZM + XANBNGHZEFZMXAUBUIZBXGGHZEFZMXAXGNUJHZBXJGHZEFZMXAWSMUAUBAXBNJZXDXFXAXMXB + NXCXEEXMOXBNBGPQRXBXGJZXDXIXAXNXBXGXCXHEXNOXBXGBGPQRXBXJJZXDXLXAXOXBXJXCX + KEXOOXBXJBGPQRXBAJZXDWSXAXPXBAXCWREXPOXBABGPQRXABNWNWOUKZNUCCXAULSXANDBXA + UMDUDCZXAUOSZXQNDEFXAUNSWNWOLZTUPXGUFCZXAXIXLYAXAXIXLYAXAXIUEZXJXHBVEHZXK + EYBXJXGBVEHZYCYBXGNYBXGYAXAXIUQZURZYBUMZUSZYBXGBYFXAYAWNXIXQUTZVAZYBXHBYB + BXGYIYBXGYEVBZVCZYIVAYBXJXGDVEHZYDYHYBXGDYFXRYBUOSZVAYJYBXJXGXGUJHYMEYBNX + GXGYGYFYFYBXGYEVDVFYBXGYBXGYFVOVGVHYBDBXGYNYIYFYBXGYKVIYAWNWOXIVJVKTYBXGX + HBYFYLYIXAYAIBEFXIXAIDBXAVLXSXQIDEFXAVMSXTTUTYAXAXIVPVNTYBBXGYBBYIVOYKVQV + HVRVSVTWAWBWPWTKZINAWREINEFYOWCSWPWTLZYOWRBIGHNYOAIBGYPWGYOBYOBWMWNWOWTUG + VOWDWEWFWMWNWQWTWHZWOWMYQAWIWJWKWL $. $} @@ -508623,6 +508767,16 @@ its graph has a given second element (that is, function value). DXEXFXGXHXIVM $. $} + $( The support of the indicator function. (Contributed by Thierry Arnoux, + 13-Oct-2025.) $) + indsupp $p |- ( ( O e. V /\ A C_ O ) -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = A ) + $= + ( wcel wss wa cind cfv cc0 csupp co ccnv c1 cpr csn cdif cima cvv wceq a1i + wf simpl c0ex fsuppeq imp syl21anc prcom difeq1i wne ax-1ne0 difprsn2 ax-mp + indf eqtri imaeq2d indpi1 3eqtrd ) BCDZABEZFZABGHHZIJKZVALZIMNZIOZPZQZVCMOZ + QAUTURIRDZBVDVAUAZVBVGSZURUSUBVIUTUCTABCUMURVIFVJVKVDVABCRIUDUEUFUTVFVHVCVF + VHSUTVFMINZVEPZVHVDVLVEIMUGUHMIUIVMVHSUJMIUKULUNTUOABCUPUQ $. + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -517553,24 +517707,290 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a VUIVUJYPVUKYPYAVUQUAFVURVULVUMVUNXM $. $} - $d .x. f i v $. $d .x. g h w $. $d A f i v $. $d A g h w $. - $d B f i v $. $d F f i v $. $d F g h $. $d M f i v $. $d M g h w $. - $d R f i v $. $d R g h $. $d X g $. $d f i ph v $. $d h i v w $. - elrgspn.1 $e |- ( ph -> X e. B ) $. + $d .x. f g h i v w y $. $d A f g h i v w $. $d B f g i v w y $. + $d F f g h i v w y $. $d M f g h i v w y $. $d R f g h i v w y $. + $d X f i g v $. $d ph f g i v w y $. $( Membership in the subring generated by the subset ` A ` . An element ` X ` lies in that subring if and only if ` X ` is a linear combination with integer coefficients of products of elements of ` A ` . (Contributed by Thierry Arnoux, 5-Oct-2025.) $) elrgspn $p |- ( ph -> ( X e. ( N ` A ) <-> E. g e. F X = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) ) $= - ( vh vv vi cfv wcel cword cv cgsu co cmpt wceq wrex fveq1 oveq1d mpteq2dv - crn fveq2 oveq2 oveq12d cbvmptv eqtrdi oveq2d rneqi elrgspnlem4 eleq2d wb - elrnmpt syl bitrd ) ALCKUDZUELUAIEBCUFZBUGZUAUGZUDZJVLUHUIZFUIZUJZUHUIZUJ - ZUPZUEZLEBVKVLHUGZUDZVOFUIZUJZUHUIZUKHIULZAVJVTLAUBCDEVTFGUCIJKMNOPQRSVSU - CIEUBVKUBUGZUCUGZUDZJWHUHUIZFUIZUJZUHUIZUJUAUCIVRWNVMWIUKZVQWMEUHWOVQBVKV - LWIUDZVOFUIZUJWMWOBVKVPWQWOVNWPVOFVLVMWIUMUNUOBUBVKWQWLVLWHUKWPWJVOWKFVLW - HWIUQVLWHJUHURUSUTVAVBUTVCVDVEALDUEWAWGVFTHIWFLVSDUAHIVRWFVMWBUKZVQWEEUHW - RBVKVPWDWRVNWCVOFVLVMWBUMUNUOVBUTVGVHVI $. + ( wcel vy vh vv vi cfv cword cv cgsu co cmpt wceq wrex csubrg wss cbs a1i + crgspn eqidd rgspncl subrgss syl sselda wa simpr cvv c0g eqid ccmn adantr + ringcmnd fvexi ssexd wrdexg cgrp ringgrpd ad2antrr cz zex cmap cc0 cfsupp + wbr breq1 elrab2 biimpi simpld adantl elmaprd ffvelcdmda cmnd crg ringmgp + sswrd mgpbas gsumwcl syl2anc mulgcld fmpttd feqmptd simprd eqbrtrrd mulg0 + fvexd fsuppssov1 gsumcl eqeltrd r19.29an crn fveq1 mpteq2dv fveq2 oveq12d + oveq1d oveq2 cbvmptv eqtrdi oveq2d rneqi elrgspnlem4 eleq2d elrnmpt bitrd + wb bibiad ) ALCKUEZTZLEBCUFZBUGZHUGZUEZJYHUHUIZFUIZUJZUHUIZUKZHIULZLDTZAY + EDLAYEEUMUETYEDUNACDEYEKRDEUOUEUKAMUPSKEUQUEUKAPUPAYEURUSYEDEMUTVAVBAYOYQ + HIAYIITZVCZYOVCLYNDYSYOVDYSYNDTYOYSYGDYMEVEEVFUEZMYTVGZAEVHTYRAERVJVIYSCV + ETZYGVETAUUBYRACDVEDVETADEUOMVKUPSVLVICVEVMVAZYSBYGYLDYSYHYGTZVCZDFEYJYKM + OAEVNTYRUUDAERVOVPYSYGVQYHYIYSYGVQYIVEVEUUCVQVETYSVRUPYRYIVQYGVSUIZTZAYRU + UGYIVTWAWBZYRUUGUUHVCGUGZVTWAWBUUHGYIUUFIUUIYIVTWAWCQWDWEZWFWGWHZWIZUUEJW + JTZYHDUFZTYKDTAUUMYRUUDAEWKTZUUMREJNWLVAVPYSYGUUNYHAYGUUNUNZYRACDUNZUUPSC + DWMVAVIVBDJYHDEJNMWNWOWPZWQWRYSBUAYJYKYGDFVQVEVTYTYSYIBYGYJUJVTWAYSBYGVQY + IUUKWSYRUUHAYRUUGUUHUUJWTWGXAUAUGZDTVTUUSFUIYTUKYSDFEUUSYTMUUAOXBWGUULUUR + YSEVFXCXDXEVIXFXGAYQVCZYFLUBIEBYGYHUBUGZUEZYKFUIZUJZUHUIZUJZXHZTZYPUUTYEU + VGLUUTUCCDEUVGFGUDIJKMNOPQAUUOYQRVIAUUQYQSVIUVFUDIEUCYGUCUGZUDUGZUEZJUVIU + HUIZFUIZUJZUHUIZUJUBUDIUVEUVOUVAUVJUKZUVDUVNEUHUVPUVDBYGYHUVJUEZYKFUIZUJU + VNUVPBYGUVCUVRUVPUVBUVQYKFYHUVAUVJXIXMXJBUCYGUVRUVMYHUVIUKUVQUVKYKUVLFYHU + VIUVJXKYHUVIJUHXNXLXOXPXQXOXRXSXTYQUVHYPYCAHIYNLUVFDUBHIUVEYNUVAYIUKZUVDY + MEUHUVSBYGUVCYLUVSUVBYJYKFYHUVAYIXIXMXJXQXOYAWGYBYD $. + $} + + ${ + elrgspnsubrun.b $e |- B = ( Base ` R ) $. + elrgspnsubrun.t $e |- .x. = ( .r ` R ) $. + elrgspnsubrun.z $e |- .0. = ( 0g ` R ) $. + elrgspnsubrun.n $e |- N = ( RingSpan ` R ) $. + elrgspnsubrun.r $e |- ( ph -> R e. CRing ) $. + elrgspnsubrun.e $e |- ( ph -> E e. ( SubRing ` R ) ) $. + elrgspnsubrun.f $e |- ( ph -> F e. ( SubRing ` R ) ) $. + + ${ + $d .0. e f w $. $d .0. y $. $d .x. d e f g w $. $d .x. y $. + $d B e y $. $d B g i w $. $d E d e f g h w $. $d E h i $. + $d F d e f g h w $. $d F h i $. $d P e f w $. $d R d e f g w $. + $d R i $. $d T e f g h w $. $d X g $. $d X i $. $d d e f g ph w $. + $d i ph $. $d ph y $. + elrgspnsubrunlem1.p1 $e |- ( ph -> P : F --> E ) $. + elrgspnsubrunlem1.p2 $e |- ( ph -> P finSupp .0. ) $. + elrgspnsubrunlem1.x $e |- ( ph + -> X = ( R gsum ( e e. F |-> ( ( P ` e ) .x. e ) ) ) ) $. + elrgspnsubrunlem1.t $e |- + T = ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) $. + $( Lemma for ~ elrgspnsubrun , first direction. (Contributed by Thierry + Arnoux, 13-Oct-2025.) $) + elrgspnsubrunlem1 $p |- ( ph -> X e. ( N ` ( E u. F ) ) ) $= + ( vw vg vh vi cun cfv wcel cword cmgp cgsu cmg cmpt wceq cc0 cfsupp wbr + cv co cmap crab wrex cind fveq1 oveq1d mpteq2dv oveq2d eqeq2d breq1 cvv + cz zex a1i csubrg unexd wrdexg syl c1 cpr wss wf csupp cs2 crn wa ssun1 + wral adantr suppssdm fssdm sselda ffvelcdmd sselid ssun2 ralrimiva eqid + sstrdi s2cld rnmptss eqsstrid indf syl2anc 0zd 1zzd prssd elmapdd ffund + fssd cfn indsupp fsuppimpd mptfi eqeltrd cdif simpr ssdifssd ffvelcdmda + subrgss eqtrd gsummptres2 fveq2 id oveq12d s2fv1 ad2antlr r19.29a s2eqd + adantl sstrd ad3antlr fveq1d fveq2d ad4ant13 syl3anc syl2an2r ad3antrrr + 3eqtr4d rnfi 3syl eqeltrid isfsuppd elrabd crngringd ringcmnd wfn fvexi + ffnd c0g fvdifsupp crg ringlzd ringcld nfcv syldan simplr eleq2i biimpi + elrnmpt2d cbvmptv elrnmpt1d eleqtrrdi 3eqtrrd eqtr2d impbida gsummptf1o + ssidd reu6dv ind0 cmnd crngmgp cmnmndd unssd sswrd mgpbas gsumwcl mulg0 + ccrg ccmn cgrp crnggrpd mulgcld mulg1 sseldd mgpplusg gsumws2 mpteq2dva + ind1 3eqtr4rd rspcedvdw cbvrabv elrgspn mpbird ) ALIJUIZKUJUKLDUEUWPULZ + UEVAZUFVAZUJZDUMUJZUWRUNVBZDUOUJZVBZUPZUNVBZUQZUFUGVAZURUSUTZUGVNUWQVCV + BZVDZVEAUXGLDUEUWQUWREUWQVFUJUJZUJZUXBUXCVBZUPZUNVBZUQUFUXLUXKUWSUXLUQZ + UXFUXPLUXQUXEUXODUNUXQUEUWQUXDUXNUXQUWTUXMUXBUXCUWRUWSUXLVGVHVIVJVKAUXI + UXLURUSUTUGUXLUXJUXHUXLURUSVLAVNUWQUXLVMVMVNVMUKAVOVPAUWPVMUKUWQVMUKZAI + JDVQUJZUXSSTVRUWPVMVSVTZAUWQURWAWBZVNUXLAUXREUWQWCZUWQUYAUXLWDUXTAEHCMW + EVBZHVAZCUJZUYDWFZUPZWGZUWQUDAUYFUWQUKZHUYCWJUYHUWQWCAUYIHUYCAUYDUYCUKZ + WHZUYEUYDUWPUYKIUWPUYEIJWIUYKJIUYDCAJICWDUYJUAWKAUYCJUYDAJIUYCCCMWLUAWM + ZWNZWOWPAUYCUWPUYDAUYCJUWPUYLJIWQWTWNXAWRHUYCUYFUWQUYGUYGWSZXBVTXCZEUWQ + VMXDXEZAURWAVNAXFZAXGXHXKZXIZAUXLUXJVNURUYSUYQAUWQUYAUXLUYPXJAUXLURWEVB + ZEXLAUXRUYBUYTEUQUXTUYOEUWQVMXMXEAEUYHXLUDAUYCXLUKUYGXLUKUYHXLUKACMUBXN + ZHUYCUYFXOUYGUUAUUBUUCZXPUUDUUEADGJGVAZCUJZVUCFVBZUPUNVBZDUEEWAUWRUJZCU + JZVUGFVBZUPZUNVBZLUXPAVUFDGUYCVUEUPUNVBVUKAGJBUYCDUXSVUEMNPADADRUUFZUUG + ZTAVUCJUYCXQZUKZWHZVUEMVUCFVBMVUPVUDMVUCFVUPJCUXSVMVUCMACJUUHVUOAJICUAU + UJWKAJUXSUKZVUOTWKMVMUKVUPMDUUKPUUIVPAVUOXRUULVHVUPBDFVUCMNOPADUUMUKZVU + OVULWKAVUNBVUCAJBUYCAVUQJBWCTJBDNYAVTZXSWNUUNYBVUAAVUCJUKZWHBDFVUDVUCNO + AVURVUTVULWKAJBVUCCAJIBCUAAIUXSUKIBWCSIBDNYAVTZXKZXTAJBVUCVUSWNUUOZUYLY + CAGUEUYCBVUEEVUGBDVUIMGVUIUUPNPVUCVUGUQZVUDVUHVUCVUGFVUCVUGCYDVVDYEZYFV + UMVUAABUVIAVUCUYCUKZVUTVUEBUKAUYCJVUCUYLWNZVVCUUQAUWREUKZWHZUWRUYFUQZVU + GUYCUKHUYCVVIUYJWHZVVJWHZVUGUYDUYCVVLVUGWAUYFUJZUYDVVJVUGVVMUQVVKWAUWRU + YFVGYKUYJVVMUYDUQZVVIVVJUYEUYDUYCYGZYHYBZVVIUYJVVJUURZXPVVIHUYCUYFUWRUY + GUYNVVHUWRUYHUKZAVVHVVREUYHUWRUDUUSUUTYKUVAZYIAVVFWHZVVDUEEVUDVUCWFZVVT + VWAUYHEVVTGUYCVWAUYGBULZHGUYCUYFVWAUYDVUCUQZUYEUYDVUDVUCUYDVUCCYDVWCYEY + JUVBAVVFXRVVTVUDVUCBVVTJBVUCCAJBCWDZVVFVVBWKVVGWOAUYCBVUCAUYCJBUYLVUSYL + ZWNXAUVCUDUVDVVTVVHWHZVVDUWRVWAUQZVWFVVDWHZVVJVWGHUYCVWHUYJWHZVVJWHZUWR + UYFVWAVWIVVJXRZVWJUYEUYDVUDVUCVWJUYDVUCCVWJVUCVUGVVMUYDVVDVVDVWFUYJVVJV + VEYMVWJWAUWRUYFVWKYNUYJVVNVWHVVJVVOYHUVEZYOVWLYJYBAVVHVVJHUYCVEVVFVVDVV + SYPYIVWFVWGWHZVUGWAVWAUJZVUCVWMWAUWRVWAVWFVWGXRYNVVFVWNVUCUQAVVHVWGVUDV + UCUYCYGYMUVFUVGUVJUVHYBUCAUXPDUEEUXNUPZUNVBVUKAUEUWQBEDVMUXNMNPVUMUXTAU + WRUWQEXQZUKZWHZUXNURUXBUXCVBZMVWRUXMURUXBUXCVWRUXRUYBVWQUXMURUQAUXRVWQU + XTWKAUYBVWQUYOWKAVWQXREUWQVMUWRUVKYQVHVWRUXBBUKZVWSMUQAUXAUVLUKZVWQUWRV + WBUKZVWTAUXAADUVTUKUXAUWAUKRDUXAUXAWSZUVMVTUVNZAVWPVWBUWRAUWQVWBEAUWPBW + CUWQVWBWCAIJBVVAVUSUVOZUWPBUVPVTZXSWNBUXAUWRBDUXAVXCNUVQZUVRZYRBUXCDUXB + MNPUXCWSZUVSVTYBVUBAUWRUWQUKZWHBUXCDUXMUXBNVXIADUWBUKVXJADRUWCWKAUWQVNU + WRUXLUYRXTAVXAVXJVXBVWTVXDAUWQVWBUWRVXFWNVXHYRUWDUYOYCAVWOVUJDUNAUEEUXN + VUIVVIWAUXBUXCVBZUXBUXNVUIVVIVWTVXKUXBUQAVXAVVHVXBVWTVXDAEVWBUWRAEUWQVW + BUYOVXFYLWNVXHYRBUXCDUXBNVXIUWEVTVVIUXMWAUXBUXCVVIUXRUYBVVHUXMWAUQAUXRV + VHUXTWKAUYBVVHUYOWKAVVHXREUWQVMUWRUWJYQVHVVIVVJVUIUXBUQHUYCVVLUXAUYFUNV + BZUYEUYDFVBZUXBVUIVVLVXAUYEBUKUYDBUKVXLVXMUQAVXAVVHUYJVVJVXDYSVVLJBUYDC + AVWDVVHUYJVVJVVBYSAUYJUYDJUKVVHVVJUYMYPWOVVLUYCBUYDAUYCBWCVVHUYJVVJVWEY + SVVQUWFBFUYEUYDUXAVXGDFUXAVXCOUWGUWHYQVVLUWRUYFUXAUNVVKVVJXRVJVVLVUHUYE + VUGUYDFVVLVUGUYDCVVPYOVVPYFUWKVVSYIYTUWIVJYBYTUWLAUEUWPBDUXCUHUFUXKUXAK + LNVXCVXIQUXIUHVAZURUSUTUGUHUXJUXHVXNURUSVLUWMVULVXEUWNUWO $. + $} + + ${ + $d .0. f p q v w $. $d .0. g w $. $d .0. q y $. $d .x. a $. + $d .x. e g $. $d .x. f p q v w $. $d .x. y $. $d B f v w y $. + $d B g $. $d E a $. $d E e g $. $d E f p q v w $. $d E h $. + $d E u $. $d E y $. $d F a $. $d F e g $. $d F f p q v w $. + $d F h $. $d F u $. $d F y $. $d G f p v w $. $d G u $. $d R a $. + $d R e g $. $d R f p q v w $. $d R y $. $d X g p $. $d X q $. + $d a e f p q w $. $d a ph $. $d e g ph $. $d f p ph q v w $. + $d f q u v w $. $d g h $. $d ph u $. $d ph y $. + elrgspnsubrunlem2.x $e |- ( ph -> X e. B ) $. + elrgspnsubrunlem2.1 $e |- ( ph -> G : Word ( E u. F ) --> ZZ ) $. + elrgspnsubrunlem2.2 $e |- ( ph -> G finSupp 0 ) $. + elrgspnsubrunlem2.3 $e |- ( ph -> X = ( R gsum ( w e. Word ( E u. F ) + |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) $. + $( Lemma for ~ elrgspnsubrun , second direction. (Contributed by Thierry + Arnoux, 13-Oct-2025.) $) + elrgspnsubrunlem2 $p |- ( ph -> E. p e. ( E ^m F ) ( p finSupp .0. + /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) ) $= + ( vq vv vy vu va ve cfv cv cgsu co c1st c2nd wceq cun cword wral cfsupp + wbr cmpt wa cmap wrex cxp wcel ccnv cima ad2antrr cvv ad3antrrr vex a1i + syl eqid ad4antr ffund sylancom xp1st adantr cdm cnvimass fdmd sseqtrid + wf cz sselda ffvelcdmd fmpttd cc0 0zd fmptssfisupp wss mulg0 fsuppssov1 + subrgss adantl nfv simpr oveq1d oveq2d eqeq2d csupp crn cfn syl2anc wfn + cdif ffnd wrel sstrd adantlr fvdifsupp sseldd eqtrd mpteq2dva cmnd ccmn + eldifad gsumwcl mulgcld gsummptres2 xp2nd 2fveq3 cbvmptv adantllr oveq2 + weq oveq12d simpllr elpreima simplbda fveq2 fvexd fnmptd simplr eqeltrd + wn cmgp csubrg cabl crngringd ringabld cnvex imaex csubg subrgsubg cgrp + csn cmg crnggrpd xpexd unexd wrdexg elmapd biimpa fvimacnvi subgmulgcld + wfun feqmptd eqbrtrrd c0g fvexi gsumsubgcl elmapdd wb breq1 nfmpt1 nfan + nfeq2 ovexd fvmpt2d mpteq2da anbi12d imafi rnfi snssi xpss2 ssun2 difxp + fsuppimpd sseqtrri sstrdi imassrn frnd sstrid relxp relss mpi relssdmrn + 3syl sscond imass2 difpreima suppssdm sseqtrrd sseqin2 biimpi eqsstrrdi + cin dminss ssdif2d eqsstrd grpmndd gsumz suppss2 ssfid isfsuppd ablcmnd + ccrg crngmgp unssd sswrd mgpbas ffvelcdmda gsummpt2co ad4ant13 mulgass2 + cmnmndd crg eqeq12d rspcdva elsnd eqtr4d eqtrdi gsummulc1 eldif fvmptd3 + syl13anc elpreimad stoic1a anasss sylan2b eldifd ssdifssd eqeq1d eqtr4i + ralrimiva cbvralvw cnveqi imaeq1i difeq2i bitri sylib r19.21bi simprbda + raleqi cnvimamptfin cop 1st2nd2 syldan eqeltrrd opelxpd ssrdv eqsstrrid + 3eqtr3d 3eqtr4d jca rspcedvd op1std op2ndd rspcedvdw mgpplusg subrgsubm + ex csubmnd gsumwun r19.29vva ac6mapd r19.29a ) ADUUAUKZBULZUMUNZVVNUEUL + ZUKZUOUKZVVQUPUKZEUNZUQZBGHURZUSZUTZMULZLVAVBZKDFHFULZVWEUKZVWGEUNZVCZU + MUNZUQZVDZMGHVEUNZVFUEGHVGZVWCVEUNZAVVPVWPVHZVDZVWDVDZVWMFHDUFVVPVIZGVW + GUUKZVGZVJZUFULZIUKZVXDVVPUKZUOUKZDUULUKZUNZVCZUMUNZVCZLVAVBZKDFHVXKVWG + EUNZVCZUMUNZUQZVDMVXLVWNVWSGHVXLDUUBUKZVXRAGVXRVHZVWQVWDSVKAHVXRVHZVWQV + WDTVKZVWSFHVXKGVWSVWGHVHZVDZVXCGVXJDVLLPADUUCVHVWQVWDVYBADADRUUDZUUEZVM + VXCVLVHZVYCVWTVXBVVPUEVNUUFUUGZVOAGDUUHUKVHZVWQVWDVYBAVXSVYHSGDUUIVPVMZ + VYCUFVXCVXIGVYCVXDVXCVHZVDZVXGCDGVXHVXENVXHVQZADUUJVHZVWQVWDVYBVYJADRUU + MZVRVYKVXFVXBVHZVXGGVHZVYCVYJVVPUVAZVYOVWRVYQVWDVYBVYJVWRVWCVWOVVPAVWQV + WCVWOVVPWGZAVWOVWCVVPVLVLAGHVXRVXRSTUUNZAVWBVLVHVWCVLVHZAGHVXRVXRSTUUOV + WBVLUUPVPZUUQUURZVSZVMVXDVXBVVPUUSVTVXFGVXAWAVPZVYCVYHVYJVYIWBVYKVWCWHV + XDIAVWCWHIWGZVWQVWDVYBVYJUBVRVYCVXCVWCVXDVYCVVPWCZVXCVWCVVPVXBWDZVWRWUF + VWCUQZVWDVYBVWRVWCVWOVVPWUBWEZVKWFZWIZWJZUUTWKVYCUFUGVXEVXGVXCGVXHWHVLW + LLVYCUFVWCVXEVXCWHWLAUFVWCVXEVCZWLVAVBZVWQVWDVYBAIWUMWLVAAUFVWCWHIUBUVB + UCUVCZVMWUJVYCWMWNVYCUGULZGVHVDWUPCVHZWLWUPVXHUNLUQZVYCGCWUPAGCWOZVWQVW + DVYBAVXSWUSSGCDNWRVPZVMWICVXHDWUPLNPVYLWPZVPWULWUDLVLVHZVYCLDUVDPUVEZVO + WQUVFWKZUVGZVWSVWEVXLUQZVDZVWFVXMVWLVXQWVFVWFVXMUVHVWSVWEVXLLVAUVIWSWVG + VWKVXPKWVGVWJVXODUMWVGFHVWIVXNVWSWVFFVWSFWTFVWEVXLFHVXKUVJUVLUVKWVGVYBV + DZVWHVXKVWGEWVGFHVXKVWEVLVWSWVFXAWVHDVXJUMUVMUVNXBUVOXCXDUVPVWSVXMVXQVW + SVXLVWNVLLWVEWVBVWSWVCVOVWSHGVXLWVDVSVWSVVPIWLXEUNZVJZXFZVXLLXEUNVWSWVJ + XGVHZWVKXGVHVWSVYQWVIXGVHZWVLVWRVYQVWDWUCWBZAWVMVWQVWDAIWLUCUWCZVKVVPWV + IUVQXHWVJUVRVPVWSHVXKFVXRWVKLVWSVWGHWVKXJZVHZVDZVXKDUFVXCLVCZUMUNZLWVRV + XJWVSDUMWVRUFVXCVXILWVRVYJVDZVXIWLVXGVXHUNZLWWAVXEWLVXGVXHWWAVWCIVLWHVX + DWLAIVWCXIZVWQVWDWVQVYJAVWCWHIUBXKZVRAVYTVWQVWDWVQVYJWUAVRWWAWMWVRVXCVW + CWVIXJZVXDWVRVXCVWTVWOWVJXJZVJZWWEVWRWVQVXCWWGWOZVWDVWRWVQVDZVXBWWFWOWW + HWWIVXBVWOWVJWCZWVKVGZXJZWWFWWIVXAWVPWOZVXBWWLWOWVQWWMVWRVWGWVPUVSWSWWM + VXBGWVPVGZWWLVXAWVPGUVTWWNGWWJXJHVGZWWNURWWLWWNWWOUWAWWJWVKGHUWBUWDUWEV + PWWIWVJWWKVWOWWIWVJVWOWOZWVJXLZWVJWWKWOWWIWVJVVPXFZVWOVVPWVIUWFVWRWWRVW + OWOWVQVWRVWCVWOVVPWUBUWGWBUWHWWPVWOXLWWQGHUWIWVJVWOUWJUWKWVJUWLUWMUWNXM + VXBWWFVWTUWOVPXNWVRWWGVWTVWOVJZVWTWVJVJZXJZWWEWVRVYQWWGWXAUQVWSVYQWVQWV + NWBVWOWVJVVPUWPVPWVRWWSVWCWVIWWTWVRWUFWWSVWCVVPVWOWDVWRWUHVWDWVQWUIVKZW + FWVRWVIWUFWOZWVIWWTWOWVRWVIVWCWUFWVRIWCZWVIVWCIWLUWQZAWXDVWCUQVWQVWDWVQ + AVWCWHIUBWEZVMWFWXBUWRWXCWVIWUFWVIUXBZWWTWXCWXGWVIUQWVIWUFUWSUWTWVIVVPU + XCUXAVPUXDUXEXMWIXOXBWWAVXGCVHZWWBLUQWWAGCVXGAWUSVWQVWDWVQVYJWUTVRWWAVX + FVWOVHZVYPWWAVWCVWOVXDVVPVWRVYRVWDWVQVYJWUBVMWVRVXCVWCVXDVWRVXCVWCWOZVW + DWVQVWRWUFVXCVWCWUGWUIWFZVKWIWJVXFGHWAZVPXPCVXHDVXGLNPVYLWPVPXQXRXCWVRD + XSVHZVYFWVTLUQAWXMVWQVWDWVQADVYNUXFVMVYFWVRVYGVOVXCUFDVLLPUXGXHXQVYAUXH + UXIUXJVWSDBVWCVVNIUKZVVOVXHUNZVCUMUNZDFHDBUFWVIVXFUPUKZVCZVIZVXAVJZWXOV + CUMUNZVCZUMUNZKVXPVWRWXPWYCUQVWDVWRWXPDBWVIWXOVCUMUNWYCVWRBVWCCWVIDVLWX + OLNPADXTVHZVWQADVYEUXKWBZAVYTVWQWUAWBZVWRVVNWWEVHZVDZWXOWLVVOVXHUNZLWYH + WXNWLVVOVXHWYHVWCIVLWHVVNWLAWWCVWQWYGWWDVKVWRVYTWYGWYFWBWYHWMVWRWYGXAZX + OXBWYHVVOCVHZWYILUQWYHVVMXSVHZVVNCUSZVHZWYKAWYLVWQWYGAVVMADUXLVHVVMXTVH + ZRDVVMVVMVQZUXMVPZUYAZVKWYHVWCWYMVVNVWRVWCWYMWOZWYGAWYSVWQAVWBCWOWYSAGH + CWUTAVXTHCWOZTHCDNWRZVPUXNVWBCUXOVPWBZWBWYHVVNVWCWVIWYJYAXPCVVMVVNCDVVM + WYPNUXPZYBZXHCVXHDVVOLNPVYLWPVPXQAWVMVWQWVOWBZVWRVVNVWCVHZVDZCVXHDWXNVV + ONVYLAVYMVWQXUFVYNVKVWRVWCWHVVNIAWUEVWQUBWBZUXQXUGWYLWYNWYKAWYLVWQXUFWY + RVKVWRVWCWYMVVNXUBWIXUDXHYCAWVIVWCWOZVWQAWXDWVIVWCWXEWXFWFWBZYDVWRBFWVI + CWXOVVSHWXRVXRDLNPWYEXUEAVXTVWQTWBZVWRVVNWVIVHZVDZCVXHDWXNVVONVYLAVYMVW + QXULVYNVKXUMVWCWHVVNIAWUEVWQXULUBVKVWRWVIVWCVVNXUJWIZWJXUMWYLWYNWYKAWYL + VWQXULWYRVKVWRWVIWYMVVNVWRWVIVWCWYMXUJXUBXMWIXUDXHYCXUMVVQVWOVHVVSHVHXU + MVWCVWOVVNVVPVWRVYRXULWUBWBXUNWJVVQGHYEVPUFBWVIWXQVVSVXDVVNUPVVPYFYGZUX + RXQWBAKWXPUQVWQVWDUDVKVWSVXOWYBDUMVWSFHVXNWYAVYCDUFVXCVXIVWGEUNZVCZUMUN + ZDBVXCWXOVCZUMUNZVXNWYAVYCXUQXUSDUMVYCXUQUFVXCVXEVVMVXDUMUNZVXHUNZVCXUS + VYCUFVXCXUPXVBVYKXUPVXEVXGVWGEUNZVXHUNZXVBVYKDUYBVHZVXEWHVHWXHVWGCVHZXU + PXVDUQAXVEVWQVWDVYBVYJVYDVRWULVWRVYBVYJWXHVWDVWRVYBVDZVYJVDZGCVXGAWUSVW + QVYBVYJWUTVMXVHWXIVYPXVHVWCVWOVXDVVPVWRVYRVYBVYJWUBVKXVGVXCVWCVXDVWRWXJ + VYBWXKWBZWIZWJWXLVPXPZYHVWRVYBXVFVWDVYJVWRHCVWGVWRVXTWYTXUKXUAVPWIZUXSC + DVXHEVXEVXGVWGNVYLOUXTUYKVYKXVAXVCVXEVXHVYKXVAVXGWXQEUNZXVCVYKVWAXVAXVM + UQBVWCVXDBUFYJZVVOXVAVVTXVMVVNVXDVVMUMYIXVNVVRVXGVVSWXQEVVNVXDUOVVPYFVV + NVXDUPVVPYFYKUYCVWRVWDVYBVYJYLWUKUYDVYKWXQVWGVXGEVWRVYBVYJWXQVWGUQVWDXV + HWXQVWGXVHVYOWXQVXAVHZXVGVYJVVPVWCXIZVYOVWRXVPVYBVYJVWRVWCVWOVVPWUBXKZV + KXVPVYJVXDVWCVHVYOVWCVXDVXBVVPYMYNZVTVXFGVXAYEZVPUYEYHXCXQXCUYFXRUFBVXC + XVBWXOUFBYJZVXEWXNXVAVVOVXHVXDVVNIYOVXDVVNVVMUMYIYKZYGUYGXCVWRVYBXURVXN + UQVWDXVGVXCCDEUFVLVXIVWGLNPOAXVEVWQVYBVYDVKVYFXVGVYGVOZXVLXVHCVXHDVXEVX + GNVYLAVYMVWQVYBVYJVYNVMXVHVWCWHVXDIVWRWUEVYBVYJXUHVKXVJWJZXVKYCXVGUFUGV + XEVXGVXCCVXHWHVLWLLXVGUFVWCVXEVXCWHWLAWUNVWQVYBWUOVKXVIXVGWMWNWUQWURXVG + WVAWSXWCXVKWVBXVGWVCVOWQUYHXNVWRVYBXUTWYAUQVWDXVGBVXCCWXTDVLWXOLNPVWRWY + DVYBWYEWBXWBXVGWXOLUQZBVXCWXTXJZXVGXVBLUQZUFVXCUHWVIUHULZVVPUKZUPUKZVCZ + VIZVXAVJZXJZUTZXWDBXWEUTZXVGXWFUFXWMXVGVXDXWMVHZVDZXVBWLXVAVXHUNZLXWQVX + EWLXVAVXHXWQVWCIVLWHVXDWLAWWCVWQVYBXWPWWDVMVWRVYTVYBXWPWYFVKXWQWMXWQVXD + VWCWVIXWQVXCVWCVXDVWRWXJVYBXWPWXKVKXWQVXDVXCXWLXVGXWPXAYAXPXWPXVGVYJVXD + XWLVHZYTZVDVXDWVIVHZYTZVXDVXCXWLUYIXVGVYJXWTXXBXVHXXAXWSXVHXXAVDZWVIVXD + VXAXWJXVGXXAXWJWVIXIZVYJXVGXXAVDZUHWVIXWIXWJVLXXEUHWTXXEXWGWVIVHVDXWHUP + YPXWJVQZYQXNXVHXXAXAXXCVXDXWJUKZWXQVXAXVGXXAXXGWXQUQZVYJXXEUHVXDXWIWXQW + VIXWJVLXXFXWGVXDUPVVPYFXVGXXAXAXXEVXFUPYPUYJZXNXXCVYOXVOXXCXVPVYJVYOVWR + XVPVYBVYJXXAXVQVMXVGVYJXXAYRXVRXHXVSVPYSUYLUYMUYNUYOUYPXOXBXWQXVACVHZXW + RLUQXWQWYLVXDWYMVHXXJAWYLVWQVYBXWPWYRVMXVGXWMWYMVXDXVGVXCWYMXWLXVGVXCVW + CWYMXVIVWRWYSVYBXUBWBXMZUYQWICVVMVXDXUCYBXHCVXHDXVALNPVYLWPVPXQUYTXWNXW + DBXWMUTXWOXWFXWDUFBXWMXVTXVBWXOLXWAUYRVUAXWDBXWMXWEXWLWXTVXCXWKWXSVXAXW + JWXRXWJBWVIVVSVCWXRUHBWVIXWIVVSXWGVVNUPVVPYFYGZXUOUYSVUBVUCZVUDVUIVUEVU + FVUGXVGWVIWXQVXAUFVWRWVMVYBXUEWBVUJXVGVVNVXCVHZVDZCVXHDWXNVVONVYLAVYMVW + QVYBXXNVYNVMXXOVWCWHVVNIVWRWUEVYBXXNXUHVKXVGVXCVWCVVNXVIWIWJXXOWYLWYNWY + KAWYLVWQVYBXXNWYRVMXVGVXCWYMVVNXXKWIXUDXHYCXVGWXTXWLVXCXXMXVGUFXWLVXCXV + GXWSVYJXVGXWSVDZVWCVXDVXBVVPVWRXVPVYBXWSXVQVKXXPWVIVWCVXDVWRXUIVYBXWSXU + JVKXVGXWSXXDXXAXXPBWVIVVSXWJVLXXPBWTXXPXULVDVVQUPYPXXLYQZXXDXWSXXAXXGVX + AVHZWVIVXDVXAXWJYMZVUHVTZXPZXXPVXFVXGWXQVUKZVXBXXPWXIVXFXYBUQXXPVWCVWOV + XDVVPVWRVYRVYBXWSWUBVKXYAWJZVXFGHVULVPXXPVXGWXQGVXAXXPWXIVYPXYCWXLVPXXP + XXGWXQVXAXVGXWSXXAXXHXXTXXIVUMXVGXWSXXDXXRXXQXXDXWSXXAXXRXXSYNVTVUNVUOY + SUYLVVGVUPVUQYDXNVURXRXCVUSVUTVVAAVVOUIULZUOUKZXYDUPUKZEUNZUQZVWABUIVWC + VWOUEVLVLXYDVVQUQZXYGVVTVVOXYIXYEVVRXYFVVSEXYDVVQUOYOXYDVVQUPYOYKXDWUAV + YSAXUFVDZVVOUJULZVWGEUNZUQZXYHUIVWOVFUJFGHXYJXYKGVHZVDZVYBVDZXYMVDZXYHX + YMUIXYKVWGVUKZVWOXYDXYRUQZXYGXYLVVOXYSXYEXYKXYFVWGEXYKVWGXYDUJVNZFVNZVV + BXYKVWGXYDXYTYUAVVCYKXDXYQXYKVWGGHXYJXYNVYBXYMYLXYOVYBXYMYRVUOXYPXYMXAV + VDXYJEUJFGHVVMVVNDEVVMWYPOVVEAWYOXUFWYQWBAGVVMVVHUKZVHZXUFAVXSYUCSGDVVM + WYPVVFVPWBAHYUBVHZXUFAVXTYUDTHDVVMWYPVVFVPWBAXUFXAVVIVVJVVKVVL $. + $} + + $d .0. f g h p v $. $d .x. d e w $. $d .x. f g h p v w $. + $d B f g h v w $. $d B i $. $d E d e w $. $d E f g h p v w $. $d E i $. + $d F d e w $. $d F f g h p v w $. $d F i $. $d N f g p v $. + $d R d e w $. $d R f g h p v w $. $d R i $. $d X f g h p v $. $d X i $. + $d d e f g h w $. $d d e ph w $. $d f g h p ph v w $. $d g h i $. + $d i ph $. $d i w $. + $( Membership in the ring span of the union of two subrings of a + commutative ring. (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + elrgspnsubrun $p |- ( ph -> ( X e. ( N ` ( E u. F ) ) + <-> E. p e. ( E ^m F ) ( p finSupp .0. + /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) ) ) $= + ( wcel co vw vg vh vv vi cun cfv cv cfsupp cmpt cgsu wceq cmap wrex cword + wbr cmgp cmg cc0 crab ccrg ad3antrrr csubrg wss crngringd cbs a1i subrgss + wa cz syl unssd crgspn eqidd rgspncl sselda ad2antrr cvv unexd wrdexg zex + elrabi ad2antlr elmaprd breq1 elrab simprbi oveq12d cbvmptv oveq2i eqeq2d + fveq2 oveq2 biimpar elrgspnsubrunlem2 eqid cbvrabv elrgspn biimpa r19.29a + csupp cs2 crn wf elmapd simplr id s2eqd elrgspnsubrunlem1 anasss r19.29an + rneqi impbida ) AIFGUFZHUGZSZKUHZJUIUPZICEGEUHZXQUGZXSDTZUJZUKTZULZVIZKFG + UMTZUNZAXPVIZICUAXNUOZUAUHZUBUHZUGZCUQUGZYJUKTZCURUGZTZUJZUKTZULZYGUBUCUH + ZUSUIUPZUCVJYIUMTZUTZYHYKUUCSZVIZYSVIZUDBCDEFGYKHIJKLMNOACVASZXPUUDYSPVBA + FCVCUGZSZXPUUDYSQVBAGUUHSZXPUUDYSRVBYHIBSUUDYSAXOBIAXOUUHSXOBVDAXNBCXOHAC + PVEZBCVFUGULALVGAFGBAUUIFBVDQFBCLVHVKAUUJGBVDRGBCLVHVKVLZHCVMUGULAOVGAXOV + NVOXOBCLVHVKVPVQUUFYIVJYKVRVRAYIVRSZXPUUDYSAXNVRSUUMAFGUUHUUHQRVSXNVRVTVK + VBVJVRSUUFWAVGUUDYKUUBSZYHYSUUAUCYKUUBWBWCWDUUDYKUSUIUPZYHYSUUDUUNUUOUUAU + UOUCYKUUBYTYKUSUIWEWFWGWCUUEICUDYIUDUHZYKUGZYMUUPUKTZYOTZUJZUKTZULYSUUEUV + AYRIUVAYRULUUEUUTYQCUKUDUAYIUUSYPUUPYJULUUQYLUURYNYOUUPYJYKWLUUPYJYMUKWMW + HWIWJVGWKWNWOAXPYSUBUUCUNAUAXNBCYOUEUBUUCYMHILYMWPYOWPOUUAUEUHZUSUIUPUCUE + UUBYTUVBUSUIWEWQUUKUULWRWSWTAYEXPKYFAXQYFSZVIZXRYDXPUVDXRVIZYDVIBXQCEXQJX + ATZXTXSXBZUJZXCDUCUBFGHIJLMNOAUUGUVCXRYDPVBAUUIUVCXRYDQVBAUUJUVCXRYDRVBUV + DGFXQXDZXRYDAUVCUVIAFGXQUUHUUHQRXEWSVQUVDXRYDXFUVEYDICUCGYTXQUGZYTDTZUJZU + KTZULUVEYCUVMIYCUVMULUVEYBUVLCUKEUCGYAUVKXSYTULZXTUVJXSYTDXSYTXQWLUVNXGWH + WIWJVGWKWSUVHUBUVFYKXQUGZYKXBZUJEUBUVFUVGUVPXSYKULZXTXSUVOYKXSYKXQWLUVQXG + XHWIXLXIXJXKXM $. $} @@ -518640,6 +519060,35 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a BCYEXEXGFGYPIWFWGVBWHWIWJWKWMWL $. $} + ${ + $d B x y $. $d K x y $. $d L x y $. $d ph x y $. + domnpropd.1 $e |- ( ph -> B = ( Base ` K ) ) $. + domnpropd.2 $e |- ( ph -> B = ( Base ` L ) ) $. + domnpropd.3 $e |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = + ( x ( +g ` L ) y ) ) $. + domnpropd.4 $e |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = + ( x ( .r ` L ) y ) ) $. + $( If two structures have the same components (properties), one is a domain + iff the other one is. (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + domnpropd $p |- ( ph -> ( K e. Domn <-> L e. Domn ) ) $= + ( cnzr wcel cv cmulr cfv co wceq wral wa eqid wo wi cdomn nzrpropd eqtr3d + c0g cbs adantr simpll eleq2d biimpar adantlr syl12anc grpidpropd ad2antrr + eqeq12d eqeq2d orbi12d imbi12d raleqbidva anbi12d isdomn 3bitr4g ) AEKLZB + MZCMZENOZPZEUFOZQZVEVIQZVFVIQZUAZUBZCEUGOZRZBVORZSFKLZVEVFFNOZPZFUFOZQZVE + WAQZVFWAQZUAZUBZCFUGOZRZBWGRZSEUCLFUCLAVDVRVQWIABCDEFGHIJUDAVPWHBVOWGADVO + WGGHUEZAVEVOLZSZVNWFCVOWGAVOWGQWKWJUHWLVFVOLZSZVJWBVMWEWNVHVTVIWAWNAVEDLZ + VFDLZVHVTQAWKWMUIWLWOWMAWOWKADVOVEGUJUKUHAWMWPWKAWPWMADVOVFGUJUKULJUMAVIW + AQWKWMABCDEFGHIUNUOZUPWNVKWCVLWDWNVIWAVEWQUQWNVIWAVFWQUQURUSUTUTVABCVOEVG + VIVOTVGTVITVBBCWGFVSWAWGTVSTWATVBVC $. + + $( If two structures have the same components (properties), one is a + integral domain iff the other one is. See also ~ domnpropd . + (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + idompropd $p |- ( ph -> ( K e. IDomn <-> L e. IDomn ) ) $= + ( ccrg wcel cdomn wa cidom crngpropd domnpropd anbi12d isidom 3bitr4g ) A + EKLZEMLZNFKLZFMLZNEOLFOLAUAUCUBUDABCDEFGHIJPABCDEFGHIJQRESFST $. + $} + ${ idomrcan.b $e |- B = ( Base ` R ) $. idomrcan.0 $e |- .0. = ( 0g ` R ) $. @@ -526999,6 +527448,21 @@ every nonzero prime ideal contains a prime element (this is a QVKWBVFVPVJVFADCVPVTVFVPUHWAUSUTVAVBVIAVHVJVITVHTVJTUEVC $. $} + ${ + $d A x y $. $d R x y $. $d ph x y $. + sraidom.1 $e |- A = ( ( subringAlg ` R ) ` V ) $. + sraidom.2 $e |- B = ( Base ` R ) $. + sraidom.3 $e |- ( ph -> R e. IDomn ) $. + sraidom.4 $e |- ( ph -> V C_ B ) $. + $( Condition for a subring algebra to be an integral domain. (Contributed + by Thierry Arnoux, 13-Oct-2025.) $) + sraidom $p |- ( ph -> A e. IDomn ) $= + ( vx vy cidom wcel cbs cfv eqidd cv cplusg oveqdr cmulr csra a1i sseqtrdi + wceq srabase wa sraaddg sramulr idompropd mpbid ) ADLMBLMHAJKDNOZDBAUKPAB + EDBEDUAOOUDAFUBZAECUKIGUCZUEAJQUKMKQUKMUFZJKDROBROABEDULUMUGSAUNJKDTOBTOA + BEDULUMUHSUIUJ $. + $} + ${ $d A x y $. $d W x y $. $d ph x y $. srasubrg.a $e |- ( ph -> A = ( ( subringAlg ` W ) ` S ) ) $. @@ -527193,6 +527657,74 @@ every nonzero prime ideal contains a prime element (this is a PUQZTJAVPVDWBAVOVQVTUMAWAWCWFUMURUT $. $} + ${ + $d B s t $. $d B s u $. $d J s t $. $d J u $. $d K s t $. $d K u $. + $d S s t $. $d S u $. $d W t $. $d W u $. $d ph s t $. $d ph u $. + exsslsb.b $e |- B = ( Base ` W ) $. + exsslsb.j $e |- J = ( LBasis ` W ) $. + exsslsb.k $e |- K = ( LSpan ` W ) $. + exsslsb.w $e |- ( ph -> W e. LVec ) $. + exsslsb.s $e |- ( ph -> S e. Fin ) $. + exsslsb.1 $e |- ( ph -> S C_ B ) $. + exsslsb.2 $e |- ( ph -> ( K ` S ) = B ) $. + $( Any finite generating set ` S ` of a vector space ` W ` contains a + basis. (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + exsslsb $p |- ( ph -> E. s e. J s C_ S ) $= + ( chash cfv wss cvv wcel cfn vu cv cpw ccnv csn cima cin cr clt cinf wceq + nfv wa clvec wpss wal ad2antrr simplr elin2d elin1d elpwid sstrd wfn clss + wi clmod lveclmod eqid lspf 3syl ffnd fniniseg simplbda syl2anc ad3antrrr + wf wne syl simpr pssssd adantr lspssv cle wbr cc0 cuz cn0 cpnf wfun hashf + cun ffun mp1i pwssfi ibi ssinss1d sselda nn0uz eleqtrdi funimassd a1i vex + hashcl sselpwd cbs fvex elsn sylibr elpreimad fnfvimad infssuzle syl2an2r + fvexi elind wn ssfid hashpss simpllr breqtrd nn0red eqeltrrd ltnled mpbid + pm2.65da neqned df-pss sylanbrc ex alrimiv w3a islbs3 biimpar syl13anc c0 + wrex elexd pwidg elpwd ne0d infssuzcl fvelima2 reximd2a ) AGUBZOPZOCUCZEU + DBUEZUFZUGZUFZUHUIUJZUKZUUCCQZGRUUHUGZDAGULZAUUCUUMSZUMZUUKUMZFUNSZUUCBQZ + UUCEPBUKZUAUBZUUCUOZUVAEPZBUOZVEZUAUPZUUCDSZAUURUUOUUKKUQUUQUUCCBUUQUUCCU + UQUUEUUGUUCUUQRUUHUUCAUUOUUKURUSZUTVAZACBQZUUOUUKMUQZVBUUQEBUCZVCZUUCUUGS + ZUUTAUVMUUOUUKAUVLFVDPZEAUURFVFSZUVLUVOEVPKFVGZUVOEBFHUVOVHJVIVJVKZUQZUUQ + UUEUUGUUCUVHUSUVMUVNUUCUVLSUUTUVLBUUCEVLVMVNUUQUVEUAUUQUVBUVDUUQUVBUMZUVC + BQZUVCBVQUVDUVTUVPUVABQUWAAUVPUUOUUKUVBAUURUVPKUVQVRVOUVTUVACBUVTUVAUUCCU + VTUVAUUCUUQUVBVSVTZUUQUULUVBUVIWAZVBZUUQUVJUVBUVKWAVBZUVAEBFHJWBVNUVTUVCB + UVTUVCBUKZUUJUVAOPZWCWDZUVTUUIWEWFPZQZUWFUWGUUISUWHAUWJUUOUUKUVBAGUUHUWIO + UUNRWGWHUEWKZOVPZOWIAWJRUWKOWLWMAUUCUUHSUMZUUDWGUWIUWMUUCTSZUUDWGSZAUUHTU + UCAUUEUUGTACTSZUUETQZLUWPUWQCTWNWOVRWPWQUUCXCZVRWRWSWTZVOUVTUWFUMZRUVAUUH + OUVTORVCZUWFAUXAUUOUUKUVBARUWKOUWLAWJXAVKZVOWAUVARSUWTUAXBXAUWTUUEUUGUVAU + VTUVAUUESUWFUVTUVACTAUWPUUOUUKUVBLVOZUWDXDWAUWTUVLUVAUUFEUUQUVMUVBUWFUVSU + QUVTUVAUVLSUWFUVTUVABRBRSUVTBFXEHXMXAUWEXDWAUWTUWFUVCUUFSUVTUWFVSUVCBUVAE + XFXGXHXIXNXJUWGUUIWEXKXLUWTUWGUUJUIWDUWHXOUWTUWGUUDUUJUIUWTUWNUVBUWGUUDUI + WDUVTUWNUWFUVTCUUCUXCUWCXPWAZUUQUVBUWFURUUCUVAXQVNUUPUUKUVBUWFXRZXSUWTUWG + UUJUWTUWGUWTUVATSUWGWGSUWTUUCUVAUXDUVTUVAUUCQUWFUWBWAXPUVAXCVRXTUWTUUDUUJ + UHUXEUWTUUDUWTUWNUWOUXDUWRVRXTYAYBYCYDYEUVCBYFYGYHYIUURUVGUUSUUTUVFYJUUCD + EBFUAHIJYKYLYMUVIAUXAUUJUUISZUUKGUUMYOUXBAUWJUUIYNVQUXFUWSAUUICOPARCUUHOU + XBACTLYPAUUEUUGCAUWPCUUESLCTYQVRAUVLCUUFEUVRACBTLMYRACEPZBUKUXGUUFSNUXGBC + EXFXGXHXIXNXJYSUUIWEYTVNGRUUJUUHOUUAVNUUB $. + $} + + ${ + $d B s $. $d B x $. $d J s $. $d J x $. $d K s $. $d K x $. $d W s $. + $d W x $. $d X s $. $d X x $. $d Y s $. $d ph s $. + lbslelsp.b $e |- B = ( Base ` W ) $. + lbslelsp.j $e |- J = ( LBasis ` W ) $. + lbslelsp.k $e |- K = ( LSpan ` W ) $. + lbslelsp.w $e |- ( ph -> W e. LVec ) $. + lbslelsp.x $e |- ( ph -> X e. J ) $. + lbslelsp.y $e |- ( ph -> Y C_ B ) $. + lbslelsp.1 $e |- ( ph -> ( K ` Y ) = B ) $. + $( The size of a basis ` X ` of a vector space ` W ` is less than the size + of a generating set ` Y ` . (Contributed by Thierry Arnoux, + 13-Oct-2025.) $) + lbslelsp $p |- ( ph -> ( # ` X ) <_ ( # ` Y ) ) $= + ( wcel cfv cle wa adantr cvv vs cfn chash wbr cv wss wceq clvec ad3antrrr + cen simplr lvecdim syl3anc hasheni ad4ant24 eqbrtrd simpr exsslsb r19.29a + syl hashss wn cpnf cxr hashxrcl pnfged cbs fvexi a1i ssexd sylan breqtrrd + hashinf pm2.61dan ) AGUBOZFUCPZGUCPZQUDZAVORZUAUEZGUFZVRUACVSVTCOZRWARZVP + VTUCPZVQQWCFVTUJUDZVPWDUGWCEUHOZFCOZWBWEAWFVOWBWAKUIAWGVOWBWALUIVSWBWAUKF + VTCEIULUMFVTUNUTVOWAWDVQQUDAWBGVTUBVAUOUPVSBGCDEUAHIJAWFVOKSAVOUQAGBUFVOM + SAGDPBUGVONSURUSAVOVBZRZVPVCVQQWIVPWIWGVPVDOAWGWHLSFCVEUTVFAGTOWHVQVCUGAG + BTBTOABEVGHVHVIMVJGTVMVKVLVN $. + $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -529058,6 +529590,362 @@ every nonzero prime ideal contains a prime element (this is a WFVOPIJLLUVHWQUVJVRUVI $. $} + ${ + fldextrspunfld.k $e |- K = ( L |`s F ) $. + fldextrspunfld.i $e |- I = ( L |`s G ) $. + fldextrspunfld.j $e |- J = ( L |`s H ) $. + fldextrspunfld.2 $e |- ( ph -> L e. Field ) $. + fldextrspunfld.3 $e |- ( ph -> F e. ( SubDRing ` I ) ) $. + fldextrspunfld.4 $e |- ( ph -> F e. ( SubDRing ` J ) ) $. + fldextrspunfld.5 $e |- ( ph -> G e. ( SubDRing ` L ) ) $. + fldextrspunfld.6 $e |- ( ph -> H e. ( SubDRing ` L ) ) $. + + ${ + fldextrspunlsp.n $e |- N = ( RingSpan ` L ) $. + fldextrspunlsp.c $e |- C = ( N ` ( G u. H ) ) $. + fldextrspunlsp.e $e |- E = ( L |`s C ) $. + fldextrspunlsp.1 $e |- ( ph -> B e. ( LBasis ` ( ( subringAlg ` J ) ` F ) + ) ) $. + fldextrspunlsp.2 $e |- ( ph -> B e. Fin ) $. + ${ + $d B a b c f u $. $d B e $. $d B h y $. $d B i $. $d F a b c f u $. + $d F e $. $d F h y $. $d F i $. $d G a c f u $. $d H a b c f u $. + $d H h y $. $d H i $. $d J b c $. $d J e $. $d K a b c f $. + $d L a b c f u $. $d L e $. $d L h y $. $d L i $. $d P a b c f $. + $d P h i $. $d X a u $. $d a b c f ph u $. $d a u x $. + $d b c f h ph u y $. $d b c f i ph u $. $d b e f ph u $. + fldextrspunlsplem.2 $e |- ( ph -> P : H --> G ) $. + fldextrspunlsplem.3 $e |- ( ph -> P finSupp ( 0g ` L ) ) $. + fldextrspunlsplem.4 $e |- ( ph + -> X = ( L gsum ( f e. H |-> ( ( P ` f ) ( .r ` L ) f ) ) ) ) $. + $( Lemma for ~ fldextrspunlsp : First direction. Part of the proof of + Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by + Thierry Arnoux, 13-Oct-2025.) $) + fldextrspunlsplem $p |- ( ph -> E. a e. ( G ^m B ) ( a finSupp ( 0g ` L + ) /\ X = ( L gsum ( b e. B |-> ( ( a ` b ) ( .r ` L ) b ) ) ) ) ) $= + ( vu vc vh vy vi ve cv cfv c0g cfsupp cmulr co cmpt cgsu wceq wa wral + wbr cmap wrex wcel csdrg ad2antrr drngringd ringcmnd ad3antrrr csubrg + eqid csubg sdrgsubrg syl subrgsubg subgsubm 3syl wf ffvelcdmd wss cbs + simpr sdrgss ressbas2 sseqtrrd ovexd simpllr elmaprd simplr subrgmcld + cvv sseldd fmpttd adantlr weq fveq2 oveq12d cbvmptv fvexd ssidd sstrd + fveq1d ad4antr ffvelcdmda ringlzd fisuppov1 wb adantl oveq2d mpteq2dv + breq1 eqtrd oveq1d mpteq2dva eqeq2d anbi12d cfn adantr simp-4r eqtr2d + sselda ringcld id oveq2i csupp cxp ciun anasss wn ad6antr csubmnd crg + csra clbs flddrngd eqbrtrid gsumsubmcl elmapdd fsuppmptdm lbsss eqidd + ccmn fvmptd3 srabase sseqtrd breq1d eqeq12d simpld gsummulc2 ringassd + rspcdva simprd eqtrdi 3eqtr4rd a1i csn fsuppimpd suppssdm fssdm sseld + wi ex adantrd imim12d ralimdv2 imp eleq1d cbvralvw sylib syl2anc xpfi + iunfi snssi iunxpssiun1 ssfid wfn eldifd fvdifsupp simp-6r ringrzd wo + ffnd cop df-br xpeq12d cbviunv eleq2i opeliun2xp 3bitr2i notbii ianor + sylbb mpjaodan an42ds an32s gsumcom3 3eqtr4d gsummulc1 3eqtrd eqtr4di + sneq eqtrid jca rspcedvd fveq1 cvsca clspn lbssp eleq2d clmod sralmod + csca ellspds bitr3d biimpa cress srasca fveq2d subg0 cmnd cdr cmnmndd + sdrgdrng subg0cl ress0g syl3anc 3eqtrrd breq2d ressmulr sravsca oveqd + eqeltrrd gsumsubm mptexd gsumsra 3eqtr3rd rexeqbidva ac6mapd r19.29a + mpbid ) AEUTZUNUTZVAZMVBVAZVCVKZVUKMQBQUTZVUMVAZVUPMVDVAZVEZVFZVGVEZV + HZVIZEIVJZPUTZVUNVCVKZOMQBVUPVVEVAZVUPVURVEZVFZVGVEZVHZVIZPHBVLVEZVMU + NGBVLVEZIVLVEZAVULVVOVNZVIZVVDVIZVVLUOBMEIVUKDVAZUOUTZVUMVAZVURVEZVFZ + VGVEZVFZVUNVCVKZOMQBMEIVVSVUQVURVEZVFZVGVEZVUPVURVEZVFZVGVEZVHZVIZPVW + EVVMVVRHBVWEMVOVAZGKUUCVAZVAZUUDVAZAHVWOVNZVVPVVDUDVPABVWRVNZVVPVVDUI + VPZVVRUOBVWDHVVRVVTBVNZVIZIHVWCMVWOVUNVUNWAZAMUULVNZVVPVVDVXBAMAMAMUA + UUEVQZVRZVSAIVWOVNZVVPVVDVXBUEVSZAHMUUAVAZVNZVVPVVDVXBAHMVTVAZVNZHMWB + VAZVNVXKAVWSVXMUDHMWCWDZHMWEHMWFWGVSVVQVXBIHVWCWHVVDVVQVXBVIZEIVWBHVX + PVUKIVNZVIZHMVURVVSVWAVURWAZAVXMVVPVXBVXQVXOVSVXRIHVUKDAIHDWHZVVPVXBV + XQUKVSVXPVXQWLZWIVXRGHVWAAGHWJVVPVXBVXQAGJWKVAZHAGJVOVAZVNZGVYBWJUBVY + BJGVYBWAWMWDAHMWKVAZWJZHVYBVHAVWSVYFUDVYEMHVYEWAZWMWDZHVYEJMSVYGWNWDW + OVSVXRBGVVTVUMVXRBGVUMVWRVYCAVWTVVPVXBVXQUIVSAVYDVVPVXBVXQUBVSVXRIVVN + VUKVULVXRIVVNVULVWOXAAVXHVVPVXBVXQUEVSVXRGBVLWPAVVPVXBVXQWQWRVYAWIWRV + VQVXBVXQWSWIXBWTXCXDVXCVWCUPIUPUTZDVAZVVTVYIVULVAZVAZVURVEZVFZVUNVCEU + PIVWBVYMEUPXEZVVSVYJVWAVYLVURVUKVYIDXFZVYOVVTVUMVYKVUKVYIVULXFZXLXGXH + VXCUPUQIVYLIHDVURXAVWOXAVYEVUNVUNVXCMVBXIZVYRVXIVXCIXJVXCVYIIVNZVIZGV + YEVYLAGVYEWJZVVPVVDVXBVYSAGIVYEAGKWKVAZIAGKVOVAZVNZGWUBWJZUCWUBKGWUBW + AZWMWDZAIVYEWJZIWUBVHAVXHWUHUEVYEMIVYGWMWDZIVYEKMTVYGWNWDZWOZWUIXKZXM + VYTBGVVTVYKVYTBGVYKVWRWUCAVWTVVPVVDVXBVYSUIXMAWUDVVPVVDVXBVYSUCXMVXCI + VVNVYIVULVXCIVVNVULVWOXAVXIVXCGBVLWPAVVPVVDVXBWQWRXNWRVVRVXBVYSWSWIXB + ZAVXTVVPVVDVXBUKVSZADVUNVCVKVVPVVDVXBULVSVXCUQUTZVYEVNZVIVYEMVURWUOVU + NVYGVXSVXDAMUUBVNZVVPVVDVXBWUPVXFXMVXCWUPWLXOXPZUUFUUGXCUUHVVQVVEVWEV + HZVVLVWNXQVVDVVQWUSVIZVVFVWFVVKVWMWUSVVFVWFXQVVQVVEVWEVUNVCYAXRWUTVVJ + VWLOWUTVVIVWKMVGWUTQBVVHVWJWUTVUPBVNZVIZVVGVWIVUPVURWVBVVGVUPVWEVAZVW + IWVBVUPVVEVWEVVQWUSWVAWSXLVVQWVAWVCVWIVHWUSVVQWVAVIZUOVUPVWDVWIBVWEXA + VWEWAZUOQXEZVWCVWHMVGWVFEIVWBVWGWVFVWAVUQVVSVURVVTVUPVUMXFXSXTXSVVQWV + AWLWVDMVWHVGWPUUMXDYBYCYDXSYEYFXDVVRVWFVWMVVRUOBVWEXAXAVWDVUNWVEABYGV + NVVPVVDUJVPVXCMVWCVGWPVVRMVBXIUUIVVROMUOBMVYNVGVEZVVTVURVEZVFZVGVEZVW + LVVROMEIVVSVUKVURVEZVFZVGVEZMUOBMUPIVYMVVTVURVEZVFVGVEZVFZVGVEZWVJAOW + VMVHVVPVVDUMVPVVRMUPIVYJVYIVURVEZVFZVGVEZMUPIMUOBWVNVFZVGVEZVFZVGVEWV + MWVQVVRWVSWWCMVGVVRUPIWVRWWBVVRVYSVIZMUOBVYJVYLVVTVURVEZVURVEZVFZVGVE + VYJMUOBWWEVFZVGVEZVURVEWWBWVRWWDBVYEMVURUOVWRWWEVYJVUNVYGVXDVXSVVRWUQ + VYSAWUQVVPVVDVXFVPZYHZAVWTVVPVVDVYSUIVSZWWDHVYEVYJAVYFVVPVVDVYSVYHVSV + VRIHVYIDAVXTVVPVVDUKVPXNXBZWWDVXBVIZVYEMVURVYLVVTVYGVXSWWDWUQVXBWWKYH + ZWWNGVYEVYLAWUAVVPVVDVYSVXBWULXMWWNBGVVTVYKWWNBGVYKVWRWUCAVWTVVPVVDVY + SVXBUIXMAWUDVVPVVDVYSVXBUCXMWWNIVVNVYIVULWWNIVVNVULVWOXAAVXHVVPVVDVYS + VXBUEXMWWNGBVLWPAVVPVVDVYSVXBYIWRVVRVYSVXBWSWIWRWWDVXBWLWIXBZWWDBVYEV + VTABVYEWJZVVPVVDVYSABIVYEABVWQWKVAZIAVWTBWWRWJUIBVWRWWRVWQWWRWAZVWRWA + ZUUJWDZAIWUBWWRWUJAVWQGKAVWQUUKZWUGUUNZYJUUOZWUIXKZVSYKZYLWWDUOUQBVVT + BGVYKVURXAVWRXAVYEVUNVUNWWDMVBXIZWXGWWLWWDBXJWXFWWDBGVYKVWRWUCWWLAWUD + VVPVVDVYSUCVSVVRIVVNVYIVULVVRIVVNVULVWOXAAVXHVVPVVDUEVPZVVRGBVLWPAVVP + VVDWSWRXNWRWWDVYKVUNVCVKZVYIMQBVUPVYKVAZVUPVURVEZVFZVGVEZVHZWWDVVCWXI + WXNVIEIVYIVYOVUOWXIVVBWXNVYOVUMVYKVUNVCVYQUUPVYOVUKVYIVVAWXMVYOYMZVYO + VUTWXLMVGVYOQBVUSWXKVYOVUQWXJVUPVURVYOVUPVUMVYKVYQXLZYCXTXSUUQYFVVQVV + DVYSWSVVRVYSWLUVAZUURWWDWUPVIVYEMVURWUOVUNVYGVXSVXDWWDWUQWUPWWKYHWWDW + UPWLXOXPUUSWWDWWAWWGMVGWWDUOBWVNWWFWWNVYEMVURVYJVYLVVTVYGVXSWWOWWDVYJ + VYEVNZVXBWWMYHWWPWXFUUTYDXSWWDVYIWWIVYJVURWWDVYIWXMWWIWWDWXIWXNWXQUVB + WXLWWHMVGQUOBWXKWWEQUOXEZWXJVYLVUPVVTVURVUPVVTVYKXFZWXSYMZXGXHYNUVCXS + UVDYDXSWVMWVTVHVVRWVLWVSMVGEUPIWVKWVRVYOVVSVYJVUKVYIVURVYPWXOXGXHYNUV + EVVRBVYEIURDVUNYOVEZURUTZVULVAZVUNYOVEZWYCUVFZYPZYQZUOUPMVWRVWOWVNVUN + VYGVXDAVXEVVPVVDVXGVPVXAWXHVVRVXBVYSWVNVYEVNVYTVYEMVURVYMVVTVYGVXSAWU + QVVPVVDVXBVYSVXFXMZVYTVYEMVURVYJVYLVYGVXSWYIVYTHVYEVYJAVYFVVPVVDVXBVY + SVYHXMVXCIHVYIDWUNXNXBZWUMYLZVXCVVTVYEVNZVYSVVRBVYEVVTAWWQVVPVVDWXEVP + YKZYHYLYRVVRURWYBWYEYQZWYBYPZWYHVVRWYNYGVNZWYBYGVNZWYOYGVNVVRWYQWYEYG + VNZURWYBVJZWYPAWYQVVPVVDADVUNULUVGVPZVVRVUMVUNYOVEZYGVNZEWYBVJZWYSVVQ + VVDXUCVVQVVCXUBEIWYBVVQVUKWYBVNZVXQVVCXUBAXUDVXQUVKVVPAWYBIVUKAIHWYBD + DVUNUVHUKUVIUVJYHVVQVUOXUBVVBVVQVUOXUBVVQVUOVIVUMVUNVVQVUOWLUVGUVLUVM + UVNUVOUVPXUBWYREURWYBEURXEZXUAWYEYGXUEVUMWYDVUNYOVUKWYCVULXFYCUVQUVRU + VSURWYBWYEUWBUVTWYTWYNWYBUWAUVTAWYHWYOWJVVPVVDAURWYBWYEWYFWYBWYCWYBVN + WYFWYBWJAWYCWYBUWCXRUWDVPUWEVVRVXBVYSVIZVVTVYIWYHVKZYSZWVNVUNVHZVVRXU + HXUFXUIVVRXUHVIZVXBVYSXUIXUJVYSVXBXUIVVRVXBVYSXUHXUIVYTXUHVIZWVNVUNVV + TVURVEVUNXUKVYMVUNVVTVURXUKVYIWYBVNZYSZVYMVUNVHVVTVYKVUNYOVEZVNZYSZXU + KXUMVIZVYMVUNVYLVURVEVUNXUQVYJVUNVYLVURXUQIDVWOXAVYIVUNADIUWFVVPVVDVX + BVYSXUHXUMAIHDUKUWLYTAVXHVVPVVDVXBVYSXUHXUMUEYTZXUQMVBXIXUQVYIIWYBVXC + VYSXUHXUMWQZXUKXUMWLUWGUWHYCXUQVYEMVURVYLVUNVYGVXSVXDAWUQVVPVVDVXBVYS + XUHXUMVXFYTXUQGVYEVYLAWUAVVPVVDVXBVYSXUHXUMWULYTXUQBGVVTVYKXUQBGVYKVW + RWUCAVWTVVPVVDVXBVYSXUHXUMUIYTAWUDVVPVVDVXBVYSXUHXUMUCYTXUQIVVNVYIVUL + XUQIVVNVULVWOXAXURXUQGBVLWPAVVPVVDVXBVYSXUHXUMUWIWRXUSWIWRVVRVXBVYSXU + HXUMYIWIXBXOYBXUKXUPVIZVYMVYJVUNVURVEVUNXUTVYLVUNVYJVURXUTBVYKVWRXAVV + TVUNXUTBGVYKXUTBGVYKVWRWUCAVWTVVPVVDVXBVYSXUHXUPUIYTZAWUDVVPVVDVXBVYS + XUHXUPUCYTXUTIVVNVYIVULXUTIVVNVULVWOXAAVXHVVPVVDVXBVYSXUHXUPUEYTXUTGB + VLWPAVVPVVDVXBVYSXUHXUPUWIWRVXCVYSXUHXUPWQWIWRUWLXVAXUTMVBXIXUTVVTBXU + NVVRVXBVYSXUHXUPYIXUKXUPWLUWGUWHXSXUTVYEMVURVYJVUNVYGVXSVXDVYTWUQXUHX + UPWYIVPVYTWXRXUHXUPWYJVPUWJYBXUHXUMXUPUWKZVYTXUHXULXUOVIZYSXVBXUGXVCX + UGVVTVYIUWMZWYHVNXVDUPWYBXUNVYIUVFZYPZYQZVNXVCVVTVYIWYHUWNXVGWYHXVDUP + URWYBXVFWYGUPURXEZXUNWYEXVEWYFXVHVYKWYDVUNYOVYIWYCVULXFYCVYIWYCUXKUWO + UWPUWQUPXUNWYBVVTUWRUWSUWTXULXUOUXAUXBXRUXCYCXUKVYEMVURVVTVUNVYGVXSVX + DVVRWUQVXBVYSXUHWWJVSVXCWYLVYSXUHWYMVPXOYBUXDUXEYRUXEYRUXFUXGVVRWVPWV + IMVGVVRUOBWVOWVHVXCIVYEMVURUPVWOVYMVVTVUNVYGVXDVXSVVRWUQVXBWWJYHVXIWY + MWYKWURUXHYDXSUXIVWKWVIMVGQUOBVWJWVHWXSVWIWVGVUPVVTVURWXSVWHVYNMVGWXS + VWHUPIVYJWXJVURVEZVFVYNEUPIVWGXVIVYOVVSVYJVUQWXJVURVYPWXPXGXHWXSUPIXV + IVYMWXSWXJVYLVYJVURWXTXSXTUXLXSWYAXGXHYNUXJUXMUXNAUSUTZVUNVCVKZVUKMQB + VUPXVJVAZVUPVURVEZVFZVGVEZVHZVIZVVCEUSIVVNUNVWOXAXVJVUMVHZXVKVUOXVPVV + BXVJVUMVUNVCYAXVRXVOVVAVUKXVRXVNVUTMVGXVRQBXVMVUSXVRXVLVUQVUPVURVUPXV + JVUMUXOYCXTXSYEYFUEAGBVLWPAVXQVIXVJVWQUYBVAZVBVAZVCVKZVUKVWQQBXVLVUPV + WQUXPVAZVEZVFZVGVEZVHZVIZUSXVSWKVAZBVLVEZVMZXVQUSVVNVMZAVXQXWJAVUKBVW + QUXQVAZVAZVNVXQXWJAXWMIVUKAWUBWWRIXWMWXCWUJAVWTXWMWWRVHUIBVWRXWLWWRVW + QWWSWWTXWLWAZUXRWDUVDUXSAQWWRXVSXWBXWHVWQXWLBVUKXVTUSXWNWWSXWHWAXVSWA + XVTWAXWBWAAGKVTVAVNZVWQUXTVNAWUDXWOUCGKWCWDZVWQGKVWQWAZUYAWDWXAUYCUYD + UYEAXWJXWKXQVXQAXWGXVQUSXWIVVNAXWHGBVLAGKGUYFVEZWKVAZXWHAWUEGXWSVHWUG + GWUBXWRKXWRWAZWUFWNWDAXWRXVSWKAVWQGKWXBWUGUYGZUYHYJYCZAXVJXWIVNZVIZXW + AXVKXWFXVPAXWAXVKXQXXCAXVTVUNXVJVCAVUNKVBVAZXWRVBVAZXVTAIVXLVNZIVXNVN + ZVUNXXEVHAVXHXXGUEIMWCWDZIMWEZIMKVUNTVXDUYIWGAKUYJVNXXEGVNZWUEXXEXXFV + HAKAKAKAVXHKUYKVNUEIMKTUYMWDZVQVRUYLAXWOGKWBVAVNXXKXWPGKWEGKXXEXXEWAZ + UYNWGWUGGWUBKXWRXXEXWTWUFXXMUYOUYPAXWRXVSVBXXAUYHUYQUYRYHXXDXWEXVOVUK + XXDMXWDVGVEKXWDVGVEZXVOXWEXXDBIXWDMKVWRAVWTXXCUIYHZAIVXJVNZXXCAXXGXXH + XXPXXIXXJIMWFWGYHXXDQBXWCIXXDWVAVIZXVMXWCIXXQVURXWBXVLVUPAVURXWBVHXXC + WVAAVURKVDVAZXWBAVXHVURXXRVHUEIMKVURVWOTVXSUYSWDZAVWQGKWXBWUGUYTZYBVP + VUAXXQIMVURXVLVUPVXSAXXGXXCWVAXXIVPXXQGIXVLAGIWJXXCWVAWUKVPXXDBGVUPXV + JXXDBGXVJVWRVYCXXOAVYDXXCUBYHAXXCXVJVVNVNAXWIVVNXVJXXBUXSUYEWRXNXBXXD + BIVUPABIWJXXCWXDYHYKWTVUBXCTVUCXXDXWDXVNMVGXXDQBXWCXVMXXDXWBVURXVLVUP + AXWBVURVHXXCAVURXXRXWBXXSXXTYJYHVUAXTXSAXXNXWEVHXXCAVWQGKXAXWDUYKXAXW + QAQBXWCVWRUIVUDXXLAGVWPXIWUGVUEYHVUFYEYFVUGYHVUJVUHVUI $. + $} + + $d B a f g h p v x $. $d C x $. $d F a h v x $. $d F y $. + $d G a f g h p v x $. $d G t u $. $d G y $. $d H a f g h p v $. + $d H t $. $d H u $. $d J v $. $d K a h v $. $d L a f g h p v x $. + $d L t $. $d L u $. $d L y $. $d N f p $. $d a f g h p ph v x $. + $d ph t v x $. $d ph u v $. $d ph x y $. + $( Lemma for ~ fldextrspunfld . The subring generated by the union of + two field extensions ` G ` and ` H ` is the vector sub- ` G ` space + generated by a basis ` B ` of ` H ` . Part of the proof of + Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by + Thierry Arnoux, 13-Oct-2025.) $) + fldextrspunlsp $p |- ( ph + -> C = ( ( LSpan ` ( ( subringAlg ` L ) ` G ) ) ` B ) ) $= + ( vx vp vf va vv vh vg csra cfv clspn cv wcel cun c0g cfsupp cmulr cmpt + wbr co cgsu wceq wa cmap wrex a1i eleq2d cbs eqid fldcrngd csdrg csubrg + sdrgsubrg syl elrgspnsubrun csca cvsca cress wss subrgss ressbas2 eqidd + srasca fveq2d eqtr2d crngringd ringcmnd cmnmndd csubg subrgsubg subg0cl + oveq1d cmnd ress0g cvv cfield clmod oveq2d eqeq2d anbi12d srabase eqtrd + mpteq2dv sstrd ad2antrr simplr elmaprd simprl weq fveq2 oveq12d cbvmptv + id eqtrdi r19.29an cif adantr simpr ffvelcdmda wn ad4antr ifclda fmpttd + fvexd ad3antrrr eldifbd eldifd fvdifsupp ifeqda sselda ssdifssd ringlzd + cdif sseldd ringcld gsummptres2 syl3anc breq2d mptexd sralmod rexeqbidv + clbs gsumsra sravsca oveqd lbsss sdrgss sseqtrrd sseqtrd ellspds simprr + cfn oveq2i fldextrspunlsplem breq1 fveq1 wf elmapdd ffund csupp suppss2 + wfn ffnd fsuppsssuppgd cdm suppssdm fdmd eqeltrd iftrued adantl fvmptd2 + sseqtrid mpteq2dva ccmn eleq1w ifbieq1d eldifad fvmptd3 crg 3syl 3eqtrd + ifcld fsuppimpd 3eqtr4d biimpar anasss rspcedvdw impbida 3bitr4rd eqrdv + jca 3bitrd ) AUFCBFKUMUNUNZUOUNZUNZAUFUPZCUQUWTFGURLUNZUQUGUPZKUSUNZUTV + CZUWTKUHGUHUPZUXBUNZUXEKVAUNZVDZVBZVEVDZVFZVGZUGFGVHVDZVIZUWTUWSUQZACUX + AUWTCUXAVFAUBVJVKAKVLUNZKUXGUHFGLUWTUXCUGUXPVMZUXGVMZUXCVMZUAAKPVNZAFKV + OUNZUQZFKVPUNZUQZSFKVQVRZAGUYAUQZGUYCUQZTGKVQZVRZVSAUIUPZUWQVTUNZUSUNZU + TVCZUWTUWQUJBUJUPZUYJUNZUYNUWQWAUNZVDZVBZVEVDZVFZVGZUIUYKVLUNZBVHVDZVIU + YJUXCUTVCZUWTKUJBUYOUYNUXGVDZVBZVEVDZVFZVGZUIFBVHVDZVIZUXOUXNAVUAVUIUIV + UCVUJAVUBFBVHAFKFWBVDZVLUNZVUBAFUXPWCZFVUMVFAUYDVUNUYEFUXPKUXQWDVRZFUXP + VULKVULVMZUXQWEVRAVULUYKVLAUWQFKAUWQWFZVUOWGZWHWIWPAUYMVUDUYTVUHAUYLUXC + UYJUTAUXCVULUSUNZUYLAKWQUQUXCFUQZVUNUXCVUSVFAKAKAKUXTWJZWKZWLAFKWMUNUQZ + VUTAUYDVVCUYEFKWNVRFKUXCUXSWOVRZVUOFUXPKVULUXCVUPUXQUXSWRUUAAVULUYKUSVU + RWHWIUUBAUYSVUGUWTAVUGUWQVUFVEVDUYSAUWQFKWSVUFWTXAUWQVMZAUJBVUEEIUMUNUN + ZUUFUNZUDUUCPAUYDUWQXAUQUYEUWQFKVVEUUDVRZVUOUUGAVUFUYRUWQVEAUJBVUEUYQAU + XGUYPUYOUYNAUWQFKVUQVUOUUHUUIXGXBWIXCXDUUEAUJUWQVLUNZUYKUYPVUBUWQUWRBUW + TUYLUIUWRVMVVIVMVUBVMUYKVMUYLVMUYPVMVVHABUXPVVIABGUXPABVVFVLUNZGABVVGUQ + ZBVVJWCUDBVVGVVJVVFVVJVMVVGVMUUJVRAGIVLUNZVVJAGUXPWCZGVVLVFAUYGVVMUYIGU + XPKUXQWDZVRZGUXPIKOUXQWEVRAVVFEIAVVFWFAEIVOUNUQZEVVLWCRVVLIEVVLVMUUKVRX + EXFUULZVVOXHZAUWQFKVUQVUOXEUUMUUNAUXNVUKAUXLVUKUGUXMAUXBUXMUQZVGZUXLVGZ + BCUXBUKDEFGHIJKLUWTUIUJMNOAKWTUQVVSUXLPXIAEHVOUNUQVVSUXLQXIAVVPVVSUXLRX + IAUYBVVSUXLSXIZAUYFVVSUXLTXIZUAUBUCAVVKVVSUXLUDXIABUUPUQVVSUXLUEXIVWAGF + UXBUYAUYAVWCVWBAVVSUXLXJXKVVTUXDUXKXLVWAUWTUXJKUKGUKUPZUXBUNZVWDUXGVDZV + BZVEVDVVTUXDUXKUUOUXIVWGKVEUHUKGUXHVWFUHUKXMZUXFVWEUXEVWDUXGUXEVWDUXBXN + VWHXQXOXPUUQXRUURXSAVUIUXNUIVUJAUYJVUJUQZVGZVUIVGZUXLULGULUPZBUQZVWLUYJ + UNZUXCXTZVBZUXCUTVCZUWTKUHGUXEVWPUNZUXEUXGVDZVBZVEVDZVFZVGUGVWPUXMUXBVW + PVFZUXDVWQUXKVXBUXBVWPUXCUTUUSVXCUXJVXAUWTVXCUXIVWTKVEVXCUHGUXHVWSVXCUX + FVWRUXEUXGUXEUXBVWPUUTWPXGXBXCXDVWKFGVWPUYAUYAAUYBVWIVUISXIAUYFVWIVUITX + IZVWKULGVWOFVWKVWLGUQZVGZVWMVWNUXCFVXFBFVWLUYJVWJBFUYJUVAZVUIVXEVWJBFUY + JVVGUYAAVVKVWIUDYAZAUYBVWISYAAVWIYBXKZXIYCAVUTVWIVUIVXEVWMYDZVVDYEYFYGZ + UVBZVWKVWQVXBVWKUYJVWPUXCUXMWSUXCVXLVWKKUSYHVWKGFVWPVXKUVCVWJVUDVUHXLVW + KGVWOULUYAUYJUXCUVDVDZUXCVWKVWLGVXMYQZUQZVGZVWMVWNUXCUXCVXPVWMVGZBUYJVV + GWSVWLUXCVWJUYJBUVFZVUIVXOVWMVWJBFUYJVXIUVGZYIAVVKVWIVUIVXOVWMUDYEVXQKU + SYHVXQVWLBVXMVXPVWMYBVXQVWLGVXMVWKVXOVWMXJYJYKYLVXPVXJVGUXCWFYMVXDUVEUV + HVWJVUDVUHVXBVWJVUDVGZVXBVUHVXTVXAVUGUWTVXTKUHVXMVWSVBZVEVDKUJVXMVUEVBZ + VEVDVXAVUGVXTVYAVYBKVEVXTVYAUHVXMUXEUYJUNZUXEUXGVDZVBVYBVXTUHVXMVWSVYDV + XTUXEVXMUQVGZVWRVYCUXEUXGVYEULUXEVWOVYCGVWPWSVWPVMZVYEULUHXMZVGZVWOVWNV + YCVYHVWMVWNUXCVYHVWLUXEBVYEVYGYBVYEUXEBUQZVYGVXTVXMBUXEVXTUYJUVIZVXMBUY + JUXCUVJVWJVYJBVFVUDVWJBFUYJVXIUVKYAUVPZYNYAUVLUVMVYGVWNVYCVFVYEVWLUXEUY + JXNZUVNXFVXTVXMGUXEVXTVXMBGVYKABGWCVWIVUDVVQXIXHZYNVYEUXEUYJYHUVOWPUVQU + HUJVXMVYDVUEUHUJXMZVYCUYOUXEUYNUXGUXEUYNUYJXNVYNXQXOXPXRXBVXTUHGUXPVXMK + UYAVWSUXCUXQUXSAKUVRUQVWIVUDVVBXIZAUYFVWIVUDTXIZVXTUXEVXNUQZVGZVWSVYIVY + CUXCXTZUXEUXGVDUXCUXEUXGVDUXCVYRVWRVYSUXEUXGVYRULUXEVWOVYSGVWPWSVYFVYGV + WMVYIVWNVYCUXCULUHBUVSVYLUVTVYRUXEGVXMVXTVYQYBUWAVYRVYIVYCUXCWSVYRUXEUY + JYHVYRKUSYHUWFUWBWPVYRVYSUXCUXEUXGVYRVYIVYCUXCUXCVYRVYIVGZBUYJVVGWSUXEU + XCVWJVXRVUDVYQVYIVXSYIAVVKVWIVUDVYQVYIUDYEVYTKUSYHVYTUXEBVXMVYRVYIYBVYT + UXEGVXMVXTVYQVYIXJYJYKYLVYRVYIYDVGUXCWFYMWPVYRUXPKUXGUXEUXCUXQUXRUXSAKU + WCUQZVWIVUDVYQVVAYIVXTVXNUXPUXEVXTGUXPVXMVXTUYFUYGVVMVYPUYHVVNUWDZYOYNY + PUWEVXTUYJUXCVWJVUDYBUWGZVXTUXEGUQZVGUXPKUXGVWRUXEUXQUXRAWUAVWIVUDWUDVV + AYIVXTGUXPUXEVWPVXTULGVWOUXPVXTVXEVGZVWMVWNUXCUXPWUEVWMVGFUXPVWNAVUNVWI + VUDVXEVWMVUOYEWUEBFVWLUYJVWJVXGVUDVXEVXIXIYCYRAUXCUXPUQVWIVUDVXEVXJAFUX + PUXCVUOVVDYRYEYFYGYCVXTGUXPUXEWUBYNYSVYMYTVXTUJBUXPVXMKVVGVUEUXCUXQUXSV + YOVWJVVKVUDVXHYAZVXTUYNBVXMYQZUQZVGZVUEUXCUYNUXGVDUXCWUIUYOUXCUYNUXGWUI + BUYJVVGWSUYNUXCVWJVXRVUDWUHVXSXIVXTVVKWUHWUFYAWUIKUSYHVXTWUHYBYLWPWUIUX + PKUXGUYNUXCUXQUXRUXSAWUAVWIVUDWUHVVAYIVXTWUGUXPUYNVXTBUXPVXMABUXPWCVWIV + UDVVRXIZYOYNYPXFWUCVXTUYNBUQZVGZUXPKUXGUYOUYNUXQUXRAWUAVWIVUDWUKVVAYIWU + LFUXPUYOAVUNVWIVUDWUKVUOYIVXTBFUYNUYJVWJVXGVUDVXIYAYCYRVXTBUXPUYNWUJYNY + SVYKYTUWHXCUWIUWJUWOUWKXSUWLUWMUWPUWN $. + $} + + fldextrspunfld.7 $e |- ( ph -> ( J [:] K ) e. NN0 ) $. + ${ + $d E b c $. $d E x y $. $d F b c $. $d F x y $. $d G b c $. + $d G x y $. $d J b c $. $d J x y $. $d K b $. $d L x y $. + $d b c ph $. $d b ph x y $. + fldextrspunfld.n $e |- N = ( RingSpan ` L ) $. + fldextrspunfld.c $e |- C = ( N ` ( G u. H ) ) $. + fldextrspunfld.e $e |- E = ( L |`s C ) $. + $( Lemma for ~ fldextrspunfld . Part of the proof of Proposition 5, + Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, + 13-Oct-2025.) $) + fldextrspunlem1 $p |- ( ph + -> ( dim ` ( ( subringAlg ` E ) ` G ) ) <_ ( J [:] K ) ) $= + ( vb vc csra cfv cldim cextdg co cle wbr clbs clvec wcel wne cdr csubrg + c0 cress csdrg sdrgdrng syl eqid wss sdrgsubrg wa biimpa syl2anc simpld + subsubrg sdrgss wceq ressbas2 sseqtrrd biimpar syl12anc sralvec syl3anc + cbs lbsex cv chash clmod cun cfield cidom fldidom idomringd eqidd unssd + csca crgspn a1i rgspncl rgspnssid unssad sralmod ressabs oveq1i 3eqtr4g + subrgss sseqtrd srasca eqtr3d eqeltrrd islvec adantr simpr dimval clspn + sylanbrc ad2antrr lbsss ad2antlr srabase eqtrd unssbd sstrd cn0 cfldext + lspssv cfn fldsdrgfld eqeltrid oveq2d brfldext syl22anc extdgval fveq2d + sylan 3eqtr2d hashclb fldextrspunlsp eqimssd resssra fveq1d clss n0limd + eqsstrrd lspcl eqeltrd lsslsp eqtr2d eqssd lbslelsp eqbrtrd breqtrrd ) + AECUFUGUGZUHUGZHIUIUJZUKULUDDHUFUGZUGZUMUGZAUUMUNUOZUUNUSUPAHUQUOZHDUTU + JZUQUOZDHURUGZUOZUUOAFJVAUGZUOZUUPSFJHNVBVCADHVAUGUOZUURQDHUUQUUQVDZVBV + CAFJURUGZUOZDUVEUOZDFVEZUUTAUVBUVFSFJVFVCAUVGDEVEZAEUVEUOZDGURUGUOZUVGU + VIVGZAEUVAUOZUVJREJVFZVCZADGVAUGUOZUVKPDGVFVCUVJUVKUVLEDJGMVKVHVIVJADHV + TUGZFAUVCDUVQVEQUVQHDUVQVDVLVCZAFJVTUGZVEZFUVQVMAUVBUVTSUVSJFUVSVDZVLZV + CZFUVSHJNUWAVNVCZVOZUVFUUTUVGUVHVGFDJHNVKVPVQZUUMDHUUQUUMVDUVDVRVSZUUNU + UMUUNVDZWAVCAUDWBZUUNUOZVGZUUJUWIWCUGZUUKUKUWKUUJUWLUKULUEUUIUMUGZAUWMU + SUPZUWJAUUIUNUOZUWNAUUIWDUOZUUIWLUGZUQUOUWOAECURUGUOZUWPABUVEUOZUVJEBVE + ZUWRAEFWEZUVSJBKAJAJWFUOZJWGUOOJWHVCWIZAUVSWJZAEFUVSAUVMEUVSVERUVSJEUWA + VLVCZUWCWKZKJWMUGVMAUAWNZBUXAKUGVMAUBWNZWOZUVOAEFBAUXAUVSJBKUXCUXDUXFUX + GUXHWPZWQZUWSUWRUVJUWTVGBEJCUCVKVPVQUUIECUUIVDWRVCZAGUWQUQACEUTUJZGUWQA + JBUTUJZEUTUJZJEUTUJZUXMGAUWSUWTUXOUXPVMUXIUXKBEJUVEWSVICUXNEUTUCWTMXAAU + UIECAUUIWJAEFCVTUGZAUXABUXQUXJABUVSVEZBUXQVMZAUWSUXRUXIBUVSJUWAXBVCZBUV + SCJUCUWAVNVCZXCWQZXDXEAUVMGUQUOREJGMVBVCXFUWQUUIUWQVDXGXLZUWMUUIUWMVDZW + AVCXHUWKUEWBZUWMUOZVGZUUJUYEWCUGZUWLUKUYGUWOUYFUUJUYHVMAUWOUWJUYFUYCXMZ + UWKUYFXIZUYEUUIUWMUYDXJVIUYGUUIVTUGZUWMUUIXKUGZUUIUYEUWIUYKVDZUYDUYLVDZ + UYIUYJUYGUWIUXQUYKUYGUWIBUXQUYGUWIFBUYGUWIUUMVTUGZFUWJUWIUYOVEZAUYFUWIU + UNUYOUUMUYOVDUWHXNZXOAFUYOVMZUWJUYFAFUVQUYOUWDAUUMDHAUUMWJUVRXPXQZXMVOA + FBVEZUWJUYFAEFBUXJXRZXMXSAUXSUWJUYFUYAXMZXCUYGUUIECUYGUUIWJAEUXQVEUWJUY + FUYBXMXPZXCZUYGUWIUYLUGZUYKUYGUWPUWIUYKVEVUEUYKVEAUWPUWJUYFUXLXMVUDUWIU + YLUYKUUIUYMUYNYBVIUYGUYKUXQVUEVUCUYGUXQBVUEVUBUWKBVUEVEUYFUWKBUWIEJUFUG + UGZXKUGZUGZVUEUWKBVUHUWKUWIBCDEFGHIJKLMNAUXBUWJOXHAUVPUWJPXHAUVCUWJQXHA + UVMUWJRXHZAUVBUWJSXHZUAUBUCAUWJXIZUWKUWJUWLXTUOZUWIYCUOZVUKUWKUUKUWLXTU + WKUUKIVTUGZUULUGZUHUGZUUMUHUGZUWLUWKHIYAULZUUKVUPVMAVURUWJAHWFUOZIWFUOZ + IHVUNUTUJZVMZVUNUUSUOZVURAHJFUTUJZWFNAUXBUVBVVDWFUOOSFJYDVIYEZAUUQIWFAV + VDDUTUJZJDUTUJZUUQIAUVBUVHVVFVVGVMSUWEFDJUVAWSVIHVVDDUTNWTLXAZAVUSUVCUU + QWFUOVVEQDHYDVIXFAUUQIVVAVVHADVUNHUTADUVSVEDVUNVMADFUVSUWEUWCXSDUVSIJLU + WAVNVCZYFXEADVUNUUSVVIUWFXFVUSVUTVGVURVVBVVCVGHIYGVPYHXHHIYIVCAVUQVUPVM + UWJAUUMVUOUHADVUNUULVVIYJYJXHAUUOUWJVUQUWLVMUWGUWIUUMUUNUWHXJYKYLZAUUKX + TUOUWJTXHXFUWJVUMVULUWIUUNYMVPVIYNZYOUWKVUEUWIVUFBUTUJZXKUGZUGZVUHUWKUW + IUYLVVMAUYLVVMVMUWJAUUIVVLXKAUVSBEJCWFUWAUCUXTUXKOYPYJXHYQUWKVUFWDUOZBV + UFYRUGZUOUWIBVEVVNVUHVMUWKUVJVVOUWKUVMUVJVUIUVNVCVUFEJVUFVDWRVCZUWKBVUH + VVPVVKUWKVVOUWIVUFVTUGZVEVUHVVPUOVVQUWKUWIUVSVVRUWKUWIFUVSUWKUWIUYOFUWK + UWJUYPVUKUYQVCAUYRUWJUYSXHVOZUWKUVBUVTVUJUWBVCXSAUVSVVRVMUWJAVUFEJAVUFW + JUXEXPXHXCVVPUWIVUGVVRVUFVVRVDVVPVDZVUGVDZUUAVIUUBUWKUWIFBVVSAUYTUWJVUA + XHXSBUWIVVPVUGVVMVUFVVLVVLVDVWAVVMVDVVTUUCVSUUDXCXHYTYTUUEUUFUUGYSVVJUU + HYS $. + + $d C x y $. $d E b $. $d E x y $. $d F b $. $d G b $. $d G x y $. + $d J b $. $d ph x y $. + $( The ring generated by the union of two field extensions is a field. + Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] + p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + fldextrspunfld $p |- ( ph -> E e. Field ) $= + ( vx vy cfield wcel csra cfv csca eqid ccrg csubrg casa cress cidom cun + cbs flddrngd drngringd eqidd csdrg wss sdrgss syl unssd crgspn wceq a1i + rgspncl subrfld eqeltrid idomcringd sdrgsubrg rgspnssid unssad subsubrg + co wa biimpar syl12anc sraassa syl2anc subrgss ressbas2 sseqtrd sraidom + cdr ressabs oveq1i 3eqtr4g srasca eqtr3d sdrgdrng eqeltrrd cldim cextdg + cxnn0 cn0 cle clvec clmod sralmod islvec sylanbrc dimcl fldextrspunlem1 + wbr xnn0lenn0nn0 syl3anc assafld srabase eqtrd cv cplusg sraaddg oveqdr + cmulr sramulr fldpropd mpbird ) ACUFUGECUHUIUIZUFUGAYBYBUJUIZYCUKZACULU + GECUMUIUGZYBUNUGACACJBUOVRZUPUCAJBOAEFUQZJURUIZJBKAJAJOUSUTZAYHVAZAEFYH + AEJVBUIZUGZEYHVCRYHJEYHUKZVDVEAFYKUGFYHVCSYHJFYMVDVEVFZKJVGUIVHAUAVIZBY + GKUIVHAUBVIZVJZVKVLZVMABJUMUIZUGZEYSUGZEBVCZYEYQAYLUUAREJVNVEAEFBAYGYHJ + BKYIYJYNYOYPVOVPZYTYEUUAUUBVSBEJCUCVQVTWAZYBECYBUKZWBWCAYBCURUIZCEUUEUU + FUKYRAEBUUFUUCABYHVCZBUUFVHAYTUUGYQBYHJYMWDVEBYHCJUCYMWEVEZWFZWGAGYCWHA + CEUOVRZGYCAYFEUOVRZJEUOVRZUUJGAYTUUBUUKUULVHYQUUCBEJYSWIWCCYFEUOUCWJMWK + AYBECAYBVAZUUIWLWMAYLGWHUGREJGMWNVEWOZAYBWPUIZWRUGZHIWQVRZWSUGUUOUUQWTX + HUUOWSUGAYBXAUGZUUPAYBXBUGZYCWHUGUURAYEUUSUUDYBECUUEXCVEUUNYCYBYDXDXEYB + XFVETABCDEFGHIJKLMNOPQRSTUAUBUCXGUUOUUQXIXJXKAUDUEBCYBUUHABUUFYBURUIUUH + AYBECUUMUUIXLXMAUDXNBUGUEXNBUGVSZUDUECXOUIYBXOUIAYBECUUMUUIXPXQAUUTUDUE + CXRUIYBXRUIAYBECUUMUUIXSXQXTYA $. + + $( Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] + p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) $) + fldextrspunlem2 $p |- ( ph -> C = ( L fldGen ( G u. H ) ) ) $= + ( cun cfldgen co cbs cfv flddrngd drngringd eqidd csdrg wcel wss sdrgss + eqid syl unssd crgspn wceq a1i fldgensdrg sdrgsubrg fldgenssid rgspnmin + csubrg cdr cress fldextrspunfld eqeltrrid syl3anbrc rgspnssid fldgenssp + rgspncl issdrg eqssd ) ABJEFUDZUEUFZAVQJUGUHZJVRBKAJAJOUIZUJZAVSUKZAEFV + SAEJULUHZUMEVSUNRVSJEVSUPZUOUQAFWCUMFVSUNSVSJFWDUOUQURZKJUSUHUTAUAVAZBV + QKUHUTAUBVAZAVRWCUMVRJVFUHZUMAVSVQJWDVTWEVBVRJVCUQAVSVQJWDVTWEVDVEAVSBV + QJWDVTAJVGUMBWHUMJBVHUFZVGUMBWCUMVTAVQVSJBKWAWBWEWFWGVNAWICVGUCACABCDEF + GHIJKLMNOPQRSTUAUBUCVIUIVJJBVOVKAVQVSJBKWAWBWEWFWGVLVMVP $. + $} + + fldextrspundgle.1 $e |- E = ( L |`s ( L fldGen ( G u. H ) ) ) $. + $( Inequality involving the degree of two different field extensions ` I ` + and ` J ` of a same field ` F ` . Part of the proof of Proposition 5, + Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, + 13-Oct-2025.) $) + fldextrspundgle $p |- ( ph -> ( E [:] I ) <_ ( J [:] K ) ) $= + ( cfv cextdg co cbs csra cldim cle cfldext wbr wceq eqid csdrg wss sdrgss + syl fldgenfldext extdgval cun crgspn cress cfldgen fldextrspunlem2 oveq2d + wcel eqtr4di fveq2d ressbas2 fveq12d fldextrspunlem1 eqbrtrrd eqbrtrd + 3syl ) ABFUAUBZFUCTZBUDTZTZUETZGHUAUBZUFABFUGUHVLVPUIAEIUCTZIDFBVRUJZKSMP + AEIUKTZVCEVRULQVRIEVSUMUNUOBFUPUNADIDEUQZIURTZTZUSUBZUDTZTZUETVPVQUFAWFVO + UEADVMWEVNAWDBUDAWDIIWAUTUBZUSUBBAWCWGIUSAWCWDCDEFGHIWBJKLMNOPQRWBUJZWCUJ + ZWDUJZVAVBSVDVEADVTVCDVRULDVMUIPVRIDVSUMDVRFIKVSVFVKVGVEAWCWDCDEFGHIWBJKL + MNOPQRWHWIWJVHVIVJ $. + $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -747901,18 +748789,6 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5 ( wn pm2.65i notnotri ) AAEBCDFG $. $} - ${ - $d A x $. - $( Every element of the power set of ` A ` is finite if and only if ` A ` - is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $) - pwssfi $p |- ( A e. V -> ( A e. Fin <-> ~P A C_ Fin ) ) $= - ( vx wcel cfn cpw wi cv wral wa simpl elpwi adantl ssfi syl2anc ralrimiva - wss dfss3 sylibr a1i pwidg adantr biimpi eleq1 rspcva ex impbid ) ABDZAED - ZAFZEQZUIUKGUHUICHZEDZCUJIZUKUIUMCUJUIULUJDZJUIULAQZUMUIUOKUOUPUIULALMAUL - NOPCUJERZSTUHUKUIUHUKJAUJDZUNUIUHURUKABUAUBUKUNUHUKUNUQUCMUMUICAUJULAEUDU - EOUFUG $. - $} - ${ iuneq2df.1 $e |- F/ x ph $. iuneq2df.2 $e |- ( ( ph /\ x e. A ) -> B = C ) $. @@ -747935,14 +748811,6 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5 ULUM $. $} - ${ - ssinss1d.1 $e |- ( ph -> A C_ C ) $. - $( Intersection preserves subclass relationship. (Contributed by Glauco - Siliprandi, 17-Aug-2020.) $) - ssinss1d $p |- ( ph -> ( A i^i B ) C_ C ) $= - ( wss cin ssinss1 syl ) ABDFBCGDFEBCDHI $. - $} - $( An element of the powerset of ` B ` intersected with anything, is a subset of ` B ` . (Contributed by Glauco Siliprandi, 17-Aug-2020.) $) elpwinss $p |- ( A e. ( ~P B i^i C ) -> A C_ B ) $= @@ -750760,20 +751628,6 @@ not even needed (it can be any class). (Contributed by Glauco FMPAUADFIJQBCDEFGUBHUBRKST $. $} - ${ - $d A x $. $d B x $. $d C x $. $d F x $. - $( Function value in an image. (Contributed by Glauco Siliprandi, - 2-Jan-2022.) $) - fvelima2 $p |- ( ( F Fn A /\ B e. ( F " C ) ) -> E. x e. ( A i^i C ) ( F ` - x ) = B ) $= - ( cima wcel wfn cv wbr wa wex cfv wceq cin wrex elimag df-rex adantrl imp - ibi sylib fnbr simprl elind wfun fnfun funbrfv sylan jca ex eximdv sylibr - sylan2 ) CEDFZGZEBHZAIZDGZURCEJZKZALZUREMCNZABDOZPZUPUTADPZVBUPVFACEDUOQU - AUTADRUBUQVBKURVDGZVCKZALZVEUQVBVIUQVAVHAUQVAVHUQVAKZVGVCVJBDURUQUTURBGUS - BURCEUCSUQUSUTUDUEUQUTVCUSUQEUFZUTVCBEUGVKUTVCURCEUHTUISUJUKULTVCAVDRUMUN - $. - $} - ${ $d A x $. $d C x $. rnmptssbi.1 $e |- F/ x ph $. @@ -753919,14 +754773,6 @@ not even needed (it can be any class). (Contributed by Glauco ( cr wcel cle wbr cif min2 syl2anc ) ABFGCFGBCHIBCJCHIDEBCKL $. $} - ${ - pnfged.1 $e |- ( ph -> A e. RR* ) $. - $( Plus infinity is an upper bound for extended reals. (Contributed by - Glauco Siliprandi, 5-Feb-2022.) $) - pnfged $p |- ( ph -> A <_ +oo ) $= - ( cxr wcel cpnf cle wbr pnfge syl ) ABDEBFGHCBIJ $. - $} - ${ xrnpnfmnf.1 $e |- ( ph -> A e. RR* ) $. xrnpnfmnf.2 $e |- ( ph -> -. A e. RR ) $. @@ -828110,26 +828956,6 @@ Basic algebraic structures (extension) -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - ${ - $d x z A $. $d x z B $. $d x z C $. $d x y z $. - $( Membership of an ordered pair in a union of Cartesian products over its - second component, analogous to ~ opeliunxp . (Contributed by AV, - 30-Mar-2019.) $) - opeliun2xp $p |- ( <. C , y >. e. U_ y e. B ( A X. { y } ) <-> - ( y e. B /\ C e. A ) ) $= - ( vx vz cv cop csn cxp wcel wa wex weq eleq2d anbi12d bitri anbi2i 3bitri - wceq ciun wrex cab wsb csb df-iun eleq2i opex nfv nfs1v nfcsb1v nfcv nfxp - df-rex nfcri nfan sbequ12 csbeq1a sneq xpeq12d eleq1 anbi2d exbidv bitrid - cbvexv1 elab opelxp an13 ancom velsn equcom anbi1i exbii sbequ12r equcoms - eqcomd equsexvw ) DAGZHZACBVRIZJZUAZKVSEGZWAKZACUBZEUCZKVRCKZAFUDZVSAFGZB - UEZWIIZJZKZLZFMZWGDBKZLZWBWFVSAECWAUFUGWEWOEVSDVRUHWEWHWCWLKZLZFMZWCVSTZW - OWEWGWDLZAMWTWDACUNXBWSAFXBFUIWHWRAWGAFUJAEWLAWJWKAWIBUKAWKULUMUOUPAFNZWG - WHWDWRWGAFUQXCWAWLWCXCBWJVTWKAWIBURZVRWIUSUTOPVEQXAWSWNFXAWRWMWHWCVSWLVAV - BVCVDVFWOFANZWHDWJKZLZLZFMWQWNXHFWNWHXFVRWKKZLZLZXIXGLZXHWMXJWHDVRWJWKVGR - XKXIXFWHLZLXLWHXFXIVHXMXGXIXFWHVIRQXIXEXGXIXCXEAWIVJAFVKQVLSVMXGWQFAXEWHW - GXFWPWGFAVNXEWJBDXEBWJBWJTAFXDVOVPOPVQQS $. - $} - ${ $d x A $. $d x B $. $d x y C $. $( Membership in a union of Cartesian products over its second component,