Algebraic closure definition and existence axiom.

set.mm

@@ -451159,6 +451159,12 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
   latexdef "Prt" as "\mathrm{Prt}";
 /* End of Rodolfo Medina's mathbox */
 
+/* Mathbox of metakunt */
+htmldef "isAlgCl" as ' isAlgCl ';
+  althtmldef "isAlgCl" as ' isAlgCl ';
+  latexdef "isAlgCl" as "\mathrm{isAlgClc}";
+/* End of metakunt's mathbox */
+
 /* Mathbox of Steven Nguyen */
 htmldef "-R" as
     " <IMG SRC='minus.gif' WIDTH=11 HEIGHT=19 ALT=' -' TITLE='-'><SUB>" +
@@ -649883,6 +649889,66 @@ fixed reference functional determined by this vector (corresponding to
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
 $)
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Definitions
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+
+  $c isAlgCl $.
+  $( Algebraic closure. $)
+  calgcl $a class isAlgCl $.
+
+  ${
+    $d k l p z f q x $.
+    $( Define the algebraic closure class.  (Contributed by metakunt,
+       11-Jan-2025.) $)
+    df-algcl $a |- isAlgCl = { <. l , k >. | ( l e. Field /\ k e. Field /\
+      ( A. p e. ( Base ` ( Poly1 ` l ) ) ( ( deg1 ` p ) e. NN ->
+      E. z e. ( Base ` l ) ( ( ( eval1 ` l ) ` p ) ` z ) = ( 0g ` l ) ) /\
+      E. f e. ( k RingHom l ) A. x e. l E. q e. ( Base ` ( Poly1 ` k ) )
+      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` l ) ) /\
+      ( ( ( eval1 ` l ) ` q ) ` ( f ` x ) ) = ( 0g ` l ) ) ) ) } $.
+  $}
+
+  ${
+    $d K f k l p q x z $.  $d L f k l p q x z $.
+    $( A field ` L ` is an algebraic closure of a field ` K ` if a ring
+       homomorphism ` f ` exists such that all polynomials ` p ` have a root
+       and all elements of ` L ` are algebraic over ` K ` .  (Contributed by
+       metakunt, 11-Jan-2025.) $)
+    isalgcl $p |- ( ( L e. Field /\ K e. Field ) -> ( L isAlgCl K <->
+      ( A. p e. ( Base ` ( Poly1 ` L ) ) ( ( deg1 ` p ) e. NN ->
+      E. z e. ( Base ` L ) ( ( ( eval1 ` L ) ` p ) ` z ) = ( 0g ` L ) ) /\
+      E. f e. ( K RingHom L ) A. x e. L E. q e. ( Base ` ( Poly1 ` K ) )
+      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` L ) ) /\
+      ( ( ( eval1 ` L ) ` q ) ` ( f ` x ) ) = ( 0g ` L ) ) ) ) ) $=
+      ( cfield wcel wa cv cfv c0g wceq cbs wrex cpl1 fveq2d eleq2d anbi12d cdg1
+      vl vk calgcl wbr cn ce1 wi wral ccom wne crh co simpl eleq1d simpr fveq1d
+      eqeq12d rexbidv2 imbi2d imbi12d ralbidv2 neeq2d 3anbi123d df-algcl brabga
+      w3a oveq12d simp1 simp2 simp3 jca31 a1i simpll simplr 3jca impbid bianabs
+      bitrd ) EHIZDHIZJZEDUDUEZGKZUALUFIZBKZWDEUGLZLZLZEMLZNZBEOLZPZUHZGEQLZOLZ
+      UIZFKZCKZUJZWOMLZUKZAKZWSLZWRWGLZLZWJNZJZFDQLZOLZPZAEUIZCDEULUMZPZJZWBWCV
+      TWAXOVGZWBXOJZUBKZHIZUCKZHIZWEWFWDXRUGLZLZLZXRMLZNZBXROLZPZUHZGXRQLZOLZUI
+      ZWTYJMLZUKZXDWRYBLZLZYENZJZFXTQLZOLZPZAXRUIZCXTXRULUMZPZJZVGXPUBUCEDUDHHX
+      RENZXTDNZJZXSVTYAWAUUEXOUUHXREHUUFUUGUNZUOUUHXTDHUUFUUGUPZUOUUHYLWQUUDXNU
+      UHYIWNGYKWPUUHWDYKIWDWPIYIWNUUHYKWPWDUUHYJWOOUUHXREQUUIRZRSUUHYHWMWEUUHYF
+      WKBYGWLUUHWFYGIWFWLIYFWKUUHYGWLWFUUHXREOUUIRSUUHYDWIYEWJUUHWFYCWHUUHWDYBW
+      GUUHXREUGUUIRZUQUQUUHXREMUUIRZURTUSUTVAVBUUHUUBXLCUUCXMUUHWSUUCIWSXMIUUBX
+      LUUHUUCXMWSUUHXTDXREULUUJUUIVHSUUHUUAXKAXREUUHXCXRIXCEIUUAXKUUHXREXCUUISU
+      UHYRXHFYTXJUUHWRYTIWRXJIYRXHUUHYTXJWRUUHYSXIOUUHXTDQUUJRRSUUHYNXBYQXGUUHY
+      MXAWTUUHYJWOMUUKRVCUUHYPXFYEWJUUHXDYOXEUUHWRYBWGUULUQUQUUMURTTUSVAVBTUSTV
+      DABCUCFGUBVEVFWBXPXQXPXQUHWBXPVTWAXOVTWAXOVIVTWAXOVJVTWAXOVKVLVMXQXPUHWBX
+      QVTWAXOVTWAXOVNVTWAXOVOWBXOUPVPVMVQVSVR $.
+  $}
+
+  ${
+    $d l K $.
+    $( The algebraic closure exists for any field.  We are sadly nowhere near
+       of proving that yet.  (Contributed by metakunt, 11-Jan-2025.) $)
+    ax-algclex $a |- ( K e. Field -> E. l l isAlgCl K ) $.
+  $}
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=