Field extensions of degree 1 (metamath#3351)

* Field extensions of degree 1 * Wording (iff)
GinoGiotto · Aug 9, 2023 · aefacec · aefacec
1 parent 244e8cc
commit aefacec
Showing 1 changed file with 157 additions and 0 deletions.
diff --git a/set.mm b/set.mm
@@ -467688,6 +467688,51 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
       WMBCDXOXQVPSVQWOYEEYBWTWHYBOWJYDWNWHYBCWIVRVSVTSWOEWTWAWBWC $.
   $}
 
+  ${
+    $d .0. a $.  $d .x. a $.  $d .x. v $.  $d B a $.  $d K a v $.  $d M a $.
+    $d S a $.  $d V a $.  $d V v $.  $d X a $.  $d a ph $.  $d ph v $.
+    lbslsp.v $e |- B = ( Base ` M ) $.
+    lbslsp.k $e |- K = ( Base ` S ) $.
+    lbslsp.s $e |- S = ( Scalar ` M ) $.
+    lbslsp.z $e |- .0. = ( 0g ` S ) $.
+    lbslsp.t $e |- .x. = ( .s ` M ) $.
+    lbslsp.m $e |- ( ph -> M e. LMod ) $.
+    lbslsp.1 $e |- ( ph -> V e. ( LBasis ` M ) ) $.
+    $( Any element of a left module ` M ` can be expressed as a linear
+       combination of the elements of a basis ` V ` of ` M ` .  (Contributed by
+       Thierry Arnoux, 3-Aug-2023.) $)
+    lbslsp $p |- ( ph -> ( X e. B <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X =
+       ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) ) $=
+      ( cfv wcel clspn cv cfsupp co cmpt cgsu wceq wa cmap wrex clbs eqid lbssp
+      wbr syl eleq2d wss lbsss ellspds bitr3d ) AIHGUASZSZTICTKUBZJUCUNIGBHBUBZ
+      VCSVDEUDUEUFUDUGUHKFHUIUDUJAVBCIAHGUKSZTZVBCUGRHVEVACGLVEULZVAULZUMUOUPAB
+      CDEFGVAHIJKVHLMNOPQAVFHCUQRHVECGLVGURUOUSUT $.
+  $}
+
+  ${
+    $d .0. y $.  $d B y $.  $d W x y $.  $d X x y $.
+    lindssn.1 $e |- B = ( Base ` W ) $.
+    lindssn.2 $e |- .0. = ( 0g ` W ) $.
+    $( Any singleton of a non-zero element is an independent set.  (Contributed
+       by Thierry Arnoux, 5-Aug-2023.) $)
+    lindssn $p |- ( ( W e. LVec /\ X e. B /\ X =/= .0. )
+      -> { X } e. ( LIndS ` W ) ) $=
+      ( vy vx clvec wcel wne csn cv cfv cdif wn wral wceq eqid c0 w3a wss cvsca
+      co clspn csca cbs clinds simp1 snssi 3ad2ant2 wa wo simpr eldifsni neneqd
+      c0g syl simpl3 sylanbrc adantr eldifad simpl2 lvecvs0or necon3abid mpbird
+      ioran nelsn difid a1i fveq2d clmod lveclmod lsp0 3syl neleqtrrd ralrimiva
+      eqtrd oveq2 sneq difeq2d eleq12d notbid ralbidv islinds2 biimpar syl12anc
+      wb ralsng ) BIJZCAJZCDKZUAZWJCLZAUBZGMZHMZBUCNZUDZWNWQLZOZBUENZNZJZPZGBUF
+      NZUGNZXFUQNZLZOZQZHWNQZWNBUHNJZWJWKWLUIZWKWJWOWLCAUJUKWMXLWPCWRUDZWNWNOZX
+      BNZJZPZGXJQZWMXSGXJWMWPXJJZULZXQDLZXOYBXODKZXOYCJPYBYDWPXHRZCDRZUMZPZYBYE
+      PYFPYHYBWPXHYBYAWPXHKWMYAUNZWPXGXHUOURUPYBCDWJWKWLYAUSUPYEYFVGUTYBYGXODYB
+      WPWRXFXGXHABCDEWRSZXFSZXGSZXHSZFWMWJYAXNVAYBWPXGXIYIVBWJWKWLYAVCVDVEVFXOD
+      VHURYBXQTXBNZYCYBXPTXBXPTRYBWNVIVJVKWMYNYCRZYAWMWJBVLJYOXNBVMXBBDFXBSZVNV
+      OVAVRVPVQWKWJXLXTWHWLXKXTHCAWQCRZXEXSGXJYQXDXRYQWSXOXCXQWQCWPWRVSYQXAXPXB
+      YQWTWNWNWQCVTWAVKWBWCWDWIUKVFWJXMWOXLULHAXFWRGWNXBXGBIXHEYJYPYKYLYMWEWFWG
+      $.
+  $}
+
   ${
     lindflbs.b $e |- B = ( Base ` W ) $.
     lindflbs.k $e |- K = ( Base ` F ) $.
@@ -468155,6 +468200,27 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
       AVKVSVJABCDEFGHIJKLMNOPQRSTUAAHUMUBVCAIUMUCVCVDVEVFVJIVSVSUNVAVGVHVI $.
   $}
 
+  ${
+    rgmoddim.1 $e |- V = ( ringLMod ` F ) $.
+    $( The left vector space induced by a ring over itself has dimension 1.
+       (Contributed by Thierry Arnoux, 5-Aug-2023.) $)
+    rgmoddim $p |- ( F e. Field -> ( dim ` V ) = 1 ) $=
+      ( cfield wcel cfv cur csn c1 wceq cdr cbs eqid crg 3syl syl3anc clspn syl
+      syl2anc cvv cldim chash clvec clbs cress csubrg ccrg isfld simplbi ressid
+      eqeltrd drngring subrgid crglmod csra rlmval eqtri sralvec clinds c0g wne
+      co wss sraring ringidcl sradrng drngunz lindssn crsp rspval fveq2i eqtr4i
+      ssidd fveq1i rsp1 syl5eqr eqidd sra1r sneqd fveq2d srabase 3eqtr3d islbs4
+      a1i sylanbrc dimval fvex hashsng ax-mp syl6eq ) ADEZBUAFZBGFZHZUBFZIWKBUC
+      EZWNBUDFZEZWLWOJWKAKEZAALFZUEVBZKEWTAUFFEZWPWKWSAUGEAUHUIZWKXAAKWTADWTMZU
+      JXCUKWKWSANEZXBXCAULZWTAXDUMOBWTAXABAUNFZWTAUOFFZCAUPUQZXAMURPZWKWNBUSFEZ
+      WNBQFZFZBLFZJWRWKWPWMXNEZWMBUTFZVAZXKXJWKBNEZXOWKXEWTWTVCZXRWKWSXEXCXFRWK
+      WTVMZBWTAWTXIXDVDSXNBWMXNMZWMMZVERWKBKEZXQWKWSXSYCXCXTBWTAWTXIXDVFSBWMXPX
+      PMZYBVGRXNBWMXPYAYDVHPWKAGFZHZXLFZWTXMXNWKWSXEYGWTJXCXFXEYGYFAVIFZFWTYFYH
+      XLYHXGQFXLAVJBXGQCVKVLVNWTAYEYHYHMXDYEMVOVPOWKYFWNXLWKYEWMWKBWTYEABXHJWKX
+      IWDZWKYEVQXTVRVSVTWKBWTAYIXTWAWBXNWQXLBWNYAWQMZXLMWCWEWNBWQYJWFSWMTEWOIJB
+      GWGWMTWHWIWJ $.
+  $}
+
   ${
     $d I j k $.  $d R j k $.  $d V j $.
     frlmdim.f $e |- F = ( R freeLMod I ) $.
@@ -469165,6 +469231,15 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
       KTVKVFUREVEAULUMCDUNUOUP $.
   $}
 
+  $( The subring algebra associated with a field extension is a vector space.
+     (Contributed by Thierry Arnoux, 3-Aug-2023.) $)
+  fldextsralvec $p |- ( E /FldExt F -> ( ( subringAlg ` E ) ` ( Base ` F ) )
+      e. LVec ) $=
+    ( cfldext wbr cdr wcel cbs cfv cress co csubrg csra clvec ccrg cfield isfld
+    wa sylib simpld eqid fldextfld1 fldextress fldextfld2 eqeltrrd fldextsubrg
+    sralvec syl3anc ) ABCDZAEFZABGHZIJZEFUJAKHFUJALHHZMFUHUIANFZUHAOFUIUMQABUAA
+    PRSUHBUKEABUBUHBEFZBNFZUHBOFUNUOQABUCBPRSUDUJABUJTUEULUJAUKULTUKTUFUG $.
+
   $( Closure of the field extension degree operation.  (Contributed by Thierry
      Arnoux, 29-Jul-2023.) $)
   extdgcl $p |- ( E /FldExt F -> ( E [:] F ) e. NN0* ) $=
@@ -469208,6 +469283,13 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
     wb ) ABCZAADEZAAAFGZPHZIZUJAJGCZUHUKAUJABUJKZLMUHANCZAOCUMUHUOAQCARSATUJAUN
     UAUBUHUIULUMUCUGAAUDUEUF $.
 
+  $( A trivial field extension has degree one.  (Contributed by Thierry Arnoux,
+     4-Aug-2023.) $)
+  extdgid $p |- ( E e. Field -> ( E [:] E ) = 1 ) $=
+    ( cfield wcel cextdg co cbs cfv csra cldim c1 cfldext wbr fldextid extdgval
+    wceq syl crglmod rlmval eqcomi rgmoddim eqtrd ) ABCZAADEZAFGAHGGZIGZJUBAAKL
+    UCUEOAMAANPAUDAQGUDARSTUA $.
+
   $( The multiplicativity formula for degrees of field extensions.  Given ` E `
      a field extension of ` F ` , itself a field extension of ` K ` , the
      degree of the extension ` E /FldExt K ` is the product of the degrees of
@@ -469239,6 +469321,81 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
     VCVFUNVDVGABLBCLUEUOURMQZUSMQZURNRUSNRVAVHKUMVIUNABOPUNVJUMBCOSUOURUMNURTEU
     NABUFPUGUOUSUNNUSTEUMBCUFSUGURUSUIUJUKUL $.
 
+  ${
+    $d E a x $.  $d E b i v x $.  $d E b u v x $.  $d F a $.  $d F b u v x $.
+    $d F i $.
+    $( If the degree of the extension ` E /FldExt F ` is ` 1 ` , then ` E ` and
+       ` F ` are identical.  (Contributed by Thierry Arnoux, 6-Aug-2023.) $)
+    extdg1id $p |- ( ( E /FldExt F /\ ( E [:] F ) = 1 ) -> E = F ) $=
+      ( vb vx vv vi co c1 wceq wa cbs cfv adantr cv wcel eqid syl cgsu ad2antrr
+      simpr vu va cfldext wbr cextdg cress fldextress wss csra c0 wne wex clvec
+      fldextsralvec lbsex n0 sylib csn chash cldim dimval sylan extdgval eqtr3d
+      clbs hash1snb biimpa syl2anc csca c0g cfsupp cvsca cmpt cmap cmulr simplr
+      eqidd csubrg fldextsubrg subrgss sravsca eqcomd ad5antr mpteq12dva oveq2d
+      wel oveqd cdr cfield fldextfld1 ccrg isfld fldextfld2 eqeltrrd drgextgsum
+      simplbi adantlr cvv cmnd crg drngring 3syl ringmnd ad4antr vex a1i elmapi
+      ad3antrrr wf adantl vsnid syl5eleqr ffvelrnd srasca eqtrd fveq2d eleqtrrd
+      sseldd lbsss eqsstr3d snss sylibr srabase ringcl syl3anc oveq12d ressmulr
+      gsumsnd eqtr4d 3eqtr3d cur cinvr cui syl2an2r eqeltrd wrex lbslsp r19.29a
+      wn exlimddv simp-5l simprbi crngcom 3eqtr2d simpld unitinvinv cdif simprd
+      invrvald sralmod0 clinds lbslinds sseldi eqneltrd nelne2 eldifsn sylanbrc
+      drnginvrn0 fveq2 eleq1d wral issubdrg rspcdva syl1111anc adantrl ringidcl
+      0nellinds eleqtrd clmod lveclmod mpbid anasss eleq2d bitrd ex ssrdv fvexd
+      ressid2 mpdan eqtr2d ) ABUCUDZABUEGZHIZJZBABKLZUFGZAUWABUWFIZUWCABUGZMUWD
+      AKLZUWEUHZUWFAIZUWDCNZUWEAUILLZVELZOZUWJCUWDUWNUJUKZUWOCULUWDUWMUMOZUWPUW
+      AUWQUWCABUNMZUWNUWMUWNPZUOQCUWNUPUQUWDUWOJZUWLDNZURZIZUWJDUWTUWOUWLUSLZHI
+      ZUXCDULZUWDUWOTZUWTUWMUTLZUXDHUWDUWQUWOUXHUXDIUWRUWLUWMUWNUWSVAVBUWDUXHHI
+      UWOUWDUWBUXHHUWAUWBUXHIUWCABVCMUWAUWCTVDMVDUWOUXEUXFUWLUWNDVFVGVHUWTUXCJZ
+      UAUWIUWEUXIUANZUWIOZUXJUWEOZUXIUXKJZENZUWMVILZVJLZVKUDZUXJUWMFUWLFNZUXNLZ
+      UXRUWMVLLZGZVMZRGZIZJZUXLEUXOKLZUWLVNGZUXMUXNUYGOZJZUXQUYDUXLUYIUXQJZUYDJ
+      UXJUYCUWEUYJUYDTUYIUYCUWEOUXQUYDUYIUYCUXAUXNLZUXABVOLZGZUWEUXIUYHUYCUYMIU
+      XKUXIUYHJZAUYBRGZAFUXBUXSUXRAVOLZGZVMZRGZUYCUYMUYNUYBUYRARUYNFUWLUYAUXBUY
+      QUWTUXCUYHVPZUYNFCWFZJUXTUYPUXSUXRUWAUXTUYPIUWCUWOUXCUYHVUAUWAUYPUXTUWAUW
+      MUWEAUWAUWMVQZUWAUWEAVRLZOZUWEUWIUHZUWEABUWEPZVSZUWEUWIAUWIPZVTQZWAWBWCWG
+      WDZWEUWTUYOUYCIZUXCUYHUWAUWOVUKUWCUWAUWOJUWMUWEFAUWFUWNUWLUYAUWMPUWAAWHOZ
+      UWOUWAAWIOZVULABWJZVUMVULAWKOZAWLZWPZQMUWAVUDUWOVUGMUWFPZUWAUWFWHOZUWOUWA
+      BUWFWHUWHUWABWIOZBWHOZABWMZVUTVVABWKOBWLWPZQWNMUWAUWOTWOWQZSUYNUYSUYKUXAU
+      YPGZUYMUYNUYQUWIVVEFAUXAWRVUHUWAAWSOZUWCUWOUXCUYHUWAAWTOZVVFUWAVUMVULVVGV
+      UNVUQAXAXBZAXCQXDUXAWROUYNDXEZXFUYNVVGUYKUWIOZUXAUWIOZVVEUWIOUXIVVGUYHUWA
+      VVGUWCUWOUXCVVHXHZMZUYNUWEUWIUYKUXIVUEUYHUWAVUEUWCUWOUXCVUIXHZMUYNUYKUYFU
+      WEUYNUWLUYFUXAUXNUYHUWLUYFUXNXIUXIUXNUYFUWLXGXJUYNUXAUXBUWLDXKUYTXLZXMUWA
+      UWEUYFIUWCUWOUXCUYHUWABUXOKUWABUWFUXOUWHUWAUWMUWEAVUBVUIXNXOXPXDXQZXRZUXI
+      VVKUYHUXIUXAUWMKLZUWIUXIUXBVVRUHUXAVVROUXIUXBUWLVVRUWTUXCTUXIUWOUWLVVRUHU
+      WDUWOUXCVPZUWLUWNVVRUWMVVRPZUWSXSQXTUXAVVRVVIYAYBUXIUWMUWEAUXIUWMVQVVNYCZ
+      XQMZUWIAUYPUYKUXAVUHUYPPZYDYEUYNUXRUXAIZJZUXSUYKUXRUXAUYPVWEUXRUXAUXNUYNV
+      WDTZXPVWFYFYHZUYNUYLUYPUYKUXAUWAUYLUYPIUWCUWOUXCUYHUWAUYLUWFVOLZUYPUWABUW
+      FVOUWHXPUWAVUDUYPVWHIVUGUWEAUWFUYPVUCVURVWCYGQYIXDWGYIYJWQUYIBWTOZUYKUWEO
+      ZUXAUWEOZUYMUWEOUWAVWIUWCUWOUXCUXKUYHUWAVUTVVAVWIVVBVVCBXAXBWCUXIUYHVWJUX
+      KVVPWQUXIVWKUXKUYHUXIUXQAYKLZUYCIZJZVWKEUYGUYNVWMVWKUXQUYNVWMJZUXAAYLLZLZ
+      VWPLZUXAUWEUYNVVGVWMUXAAYMLZOZVWRUXAIVVMVWOVWTVWQUYKIZVWOUWIAUYPVWSVWLVWP
+      UXAUYKVUHVWCVWLPZVWSPZVWPPZVWOUWAVVGUWAUWCUWOUXCUYHVWMUUAZVVHQUYNVVKVWMVW
+      BMZUYNVVJVWMVVQMZVWOUXAUYKUYPGZVVEVWLVWOVUOVVKVVJVXHVVEIVWOUWAVUMVUOVXEVU
+      NVUMVULVUOVUPUUBXBVXFVXGUWIAUYPUXAUYKVUHVWCUUCYEVWOVWLUYSVVEVWOVWLUYCUYOU
+      YSUYNVWMTUWTVUKUXCUYHVWMVVDXHVWOUYBUYRARUYNUYBUYRIVWMVUJMWEUUDUYNUYSVVEIV
+      WMVWGMXOZYIVWOVWLVVEVXIWBUUIZUUEAVWSVWPUXAVXCVXDUUFYNVWOVULVUDVUSVWQUWEAV
+      JLZURUUGZOZVWRUWEOZVWOUWAVUMVULVXEVUNVUQXBZVWOUWAVUDVXEVUGQVWOBUWFWHVWOUW
+      AUWGVXEUWHQVWOUWAVUTVVAVXEVVBVVCXBWNVWOVWQUWEOVWQVXKUKZVXMVWOVWQUYKUWEVWO
+      VWTVXAVXJUUHUYNVWJVWMVVPMYOVWOVULVVKUXAVXKUKZVXPVXOVXFUYNDCWFVWMVXKUWLOYS
+      ZVXQVVOUWTVXRUXCUYHVWMUWTVXKUWMVJLZUWLUWAVXKVXSIUWCUWOUWAUWMUWEAVXKVUBUWA
+      VXKVQVUIUUJSUWDUWQUWOUWLUWMUUKLZOVXSUWLOYSUWRUWTUWNVXTUWLUWNUWMUWSUULUXGU
+      UMUWLUWMVXSVXSPUVGYNUUNXHUXAVXKUWLUUOYNUWIAVWPUXAVXKVUHVXKPZVXDUURYEVWQUW
+      EVXKUUPUUQVULVUDJZVUSJZVXMJUBNZVWPLZUWEOZVXNUBVXLVWQVYDVWQIVYEVWRUWEVYDVW
+      QVWPUUSUUTVYCVYFUBVXLUVAZVXMVYBVUSVYGUBUWEAUWFVWPVXKVURVYAVXDUVBVGMVYCVXM
+      TUVCUVDWNUVEUXIVWLVVROVWNEUYGYPUXIVWLUWIVVRUXIVVGVWLUWIOVVLUWIAVWLVUHVXBU
+      VFQVWAUVHUXIFVVRUXOUXTUYFUWMUWLVWLUXPEVVTUYFPZUXOPZUXPPZUXTPZUXIUWQUWMUVI
+      OUWDUWQUWOUXCUWRSUWMUVJQZVVSYQUVKYRSUWEBUYLUYKUXAVUFUYLPYDYEYOSYOUVLUXIUX
+      KUYEEUYGYPZUXIUXKUXJVVROVYMUXIUWIVVRUXJVWAUVMUXIFVVRUXOUXTUYFUWMUWLUXJUXP
+      EVVTVYHVYIVYJVYKVYLVVSYQUVNVGYRUVOUVPYTYTUWDUWJJZUWJVUMUWEWROUWKUWDUWJTUW
+      AVUMUWCUWJVUNSVYNBKUVQUWEUWIUWFAWIWRVURVUHUVRYEUVSUVT $.
+  $}
+
+  $( The degree of the extension ` E /FldExt F ` is ` 1 ` iff ` E ` and ` F `
+     are the same structure.  (Contributed by Thierry Arnoux, 6-Aug-2023.) $)
+  extdg1b $p |- ( E /FldExt F -> ( ( E [:] F ) = 1 <-> E = F ) ) $=
+    ( cfldext cextdg co c1 wceq extdg1id wa oveq1 adantl cfield wcel fldextfld2
+    wbr adantr extdgid syl eqtrd impbida ) ABCOZABDEZFGABGZABHUAUCIZUBBBDEZFUCU
+    BUEGUAABBDJKUDBLMZUEFGUAUFUCABNPBQRST $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=