text:
:: Field Extensions and {K}ronecker's Construction
::  by Christoph Schwarzweller

environ

 vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, XCMPLX_0, VECTSP_2,
      STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1, INT_1, ALGSEQ_1, FINSET_1,
      MESFUNC1, INT_3, REALSET1, C0SP1, GAUSSINT, NAT_1, WAYBEL20, MOD_4,
      POLYNOM1, POLYNOM2, POLYNOM3, POLYNOM8, COMPLFLD, FUNCSDOM, GROEB_2,
      EC_PF_1, HURWITZ, FINSEQ_1, RING_4, GROUP_1, FUNCT_2, ARYTM_1, CARD_3,
      FUNCT_1, RELAT_1, FUNCOP_1, CARD_1, IDEAL_1, QUOFIELD, FDIFF_1, EQREL_1,
      XBOOLE_0, NUMBERS, POLYNOM5, RING_2, RING_3, GROUP_6, FUNCT_4, ZFMISC_1,
      XXREAL_0, FUNCT_7, YELLOW_8, ALGNUM_1, MSSUBFAM, RING_5, ORDINAL1,
      GROUP_2, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, FIELD_1, FIELD_2,
      FIELD_3, FIELD_4, FOMODEL1;
 notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, RELSET_1, REALSET1,
      FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, NUMBERS, ZFMISC_1, FUNCT_7,
      EQREL_1, ORDINAL1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, INT_1, INT_3,
      GAUSSINT, VFUNCT_1, IDEAL_1, COMPLFLD, POLYNOM1, ALGSEQ_1, POLYNOM3,
      POLYNOM4, POLYNOM5, FINSET_1, RINGCAT1, GROUP_1, GROUP_6, MOD_4,
      RLVECT_1, ALGSTR_0, STRUCT_0, HURWITZ, MATRLIN, VECTSP_6, VECTSP_7,
      VECTSP_9, VECTSP_2, VECTSP_1, C0SP1, EC_PF_1, RATFUNC1, QUOFIELD, RING_1,
      RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_2, FIELD_3;
 constructors REAL_1, FINSOP_1, BINARITH, VECTSP_2, POLYNOM3, ALGSTR_1,
      MCART_1, NUMBERS, RING_1, ZFMISC_1, RELAT_1, XREAL_0, HURWITZ, VALUED_0,
      STRUCT_0, C0SP1, GCD_1, COMPLFLD, FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0,
      XXREAL_0, SUBSET_1, ORDINAL1, NAT_1, ALGSTR_0, POLYNOM4, XBOOLE_0,
      RELSET_1, ARYTM_3, FUNCT_7, NAT_D, FINSEQ_1, VFUNCT_1, CARD_1, FINSET_1,
      GAUSSINT, RATFUNC1, GROUP_6, REALSET1, UPROOTS, TSEP_1, ALGSTR_2, INT_3,
      RINGCAT1, MEMBERED, IDEAL_1, RING_3, EC_PF_1, ALGSEQ_1, RING_2, VECTSP_9,
      EQREL_1, RING_4, FUNCOP_1, GROUP_4, ALGNUM_1, MOD_4, RING_5, VECTSP_6,
      FIELD_1, FIELD_2, FIELD_3;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
      STRUCT_0, VECTSP_1, ALGSTR_1, VFUNCT_1, POLYNOM4, FUNCT_2, ALGSTR_0,
      POLYNOM3, SUBSET_1, RLVECT_1, COMPLFLD, FUNCT_1, FINSET_1, INT_3,
      RATFUNC1, GAUSSINT, RELAT_1, MOD_4, RING_2, RING_3, RING_4, RING_5,
      REALSET1, FIELD_2, FIELD_3;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions ALGSTR_0, VECTSP_1, RLVECT_1;
 equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1;
 expansions STRUCT_0, GROUP_1, VECTSP_1, RINGCAT1, TARSKI, GROUP_6, FUNCT_1,
      FUNCT_2, RING_4;
 theorems GROUP_1, VECTSP_2, RLVECT_1, IDEAL_1, GCD_1, C0SP1, SUBSET_1,
      FUNCT_2, TARSKI, FUNCT_1, RELAT_1, POLYNOM1, EC_PF_1, POLYNOM4, ZFMISC_1,
      GAUSSINT, ALGSEQ_1, RING_2, POLYNOM3, ALGNUM_1, NAT_1, RING_3, XXREAL_0,
      XBOOLE_1, FINSEQ_1, NORMSP_1, RING_4, HURWITZ, XREAL_1, XREAL_0, MATRLIN,
      POLYNOM5, XBOOLE_0, UPROOTS, RATFUNC1, RINGCAT1, STRUCT_0, RING_1,
      RING_5, FIELD_1, FIELD_2, ALGSTR_0, VECTSP_1, VECTSP_6, VECTSP_7,
      VECTSP_4, ORDINAL1, FIELD_3, LIOUVIL2;
 schemes FUNCT_2;

begin :: Preliminaries

 reserve K,F,E for Field,
         R,S for Ring;

Th1:
   R is Subring of R by LIOUVIL2:18;

theorem
   K is Subfield of K
   proof
A1:  the addF of K = (the addF of K) || the carrier of K;
A2:  the multF of K = (the multF of K) || the carrier of K;
     the carrier of K c= the carrier of K & 1.K = 1.K & 0.K = 0.K;
     hence thesis by A1,A2,EC_PF_1:def 1;
   end;

registration
  let R be non degenerated Ring;
  cluster -> non degenerated for Subring of R;
  coherence
  proof
    let S be Subring of R;
    0.R = 0.S & 1.R = 1.S by C0SP1:def 3;
    hence thesis;
  end;
end;

registration
  let R be comRing;
  cluster -> commutative for Subring of R;
  coherence
  proof
    let S be Subring of R;
    now let a,b be Element of S;
      the carrier of S c= the carrier of R by C0SP1:def 3; then
      reconsider x = a, y = b as Element of R;
A1:   [x,y] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
A2:   [y,x] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
      thus
      a * b = ((the multF of R)||the carrier of S).(x,y) by C0SP1:def 3
      .= x * y by A1,FUNCT_1:49
      .= y * x by GROUP_1:def 12
      .= ((the multF of R)||the carrier of S).(b,a) by A2,FUNCT_1:49
      .= b * a by C0SP1:def 3;
    end;
    hence thesis;
  end;
end;

registration
  let R be domRing;
  cluster -> domRing-like for Subring of R;
  coherence
  proof
    let S be Subring of R;
    now let a,b be Element of S;
      assume
A1:   a * b = 0.S;
      the carrier of S c= the carrier of R by C0SP1:def 3; then
      reconsider x = a, y = b as Element of R;
A2:   [x,y] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
A3:   0.S = 0.R by C0SP1:def 3;
      a * b = ((the multF of R)||the carrier of S).(x,y) by C0SP1:def 3
      .= x * y by A2,FUNCT_1:49;
      hence a = 0.S or b = 0.S by A1,A3,VECTSP_2:def 1;
    end;
    hence thesis by VECTSP_2:def 1;
  end;
end;

theorem Th2:
   for S being Subring of R, F being FinSequence of R, G being FinSequence of S
   st F = G holds Sum F = Sum G
   proof
     let S be Subring of R, F be FinSequence of R, G be FinSequence of S;
     assume
A1:  F = G;
     the carrier of S c= the carrier of R by C0SP1:def 3; then
     In(Sum G,R) = Sum G by SUBSET_1:def 8;
     hence thesis by A1,ALGNUM_1:10;
   end;

begin :: Ring and Field Extensions

definition
  let R,S be Ring;
  attr S is R-extending means :Def1:
  R is Subring of S;
end;

registration
  let R be Ring;
  cluster R-extending for Ring;
  existence
  proof
    take R;
    thus thesis by Th1;
  end;
end;

registration
  let R be comRing;
  cluster R-extending for comRing;
  existence
  proof
    take R;
    thus thesis by Th1;
  end;
end;

registration
  let R be domRing;
  cluster R-extending for domRing;
  existence
  proof
    take R;
    thus thesis by Th1;
  end;
end;

registration
  let F be Field;
  cluster F-extending for Field;
  existence
  proof
    take F;
    thus thesis by Th1;
  end;
end;

definition
  let R be Ring;
  mode RingExtension of R is R-extending Ring;
end;

definition
  let R be comRing;
  mode comRingExtension of R is R-extending comRing;
end;

definition
  let R be domRing;
  mode domRingExtension of R is R-extending domRing;
end;

definition
  let F be Field;
  mode FieldExtension of F is F-extending Field;
end;

theorem
   R is RingExtension of R
   proof
     R is Subring of R by Th1;
     hence thesis by Def1;
   end;

theorem
   for R being comRing holds R is comRingExtension of R
   proof
     let R be comRing;
     R is Subring of R by Th1;
     hence thesis by Def1;
   end;

theorem
   for R being domRing holds R is domRingExtension of R
   proof
     let R be domRing;
     R is Subring of R by Th1;
     hence thesis by Def1;
   end;

theorem Th3:
   F is FieldExtension of F
   proof
     F is Subring of F by Th1;
     hence thesis by Def1;
   end;

theorem Th4:
   E is FieldExtension of F iff F is Subfield of E
   proof
A1:  now assume E is FieldExtension of F; then
       F is Subring of E by Def1;
       hence F is Subfield of E by RING_3:45;
     end;
     now assume F is Subfield of E; then
       F is Subring of E by RING_3:43;
       hence E is FieldExtension of F by Def1;
     end;
     hence thesis by A1;
   end;

registration
  cluster F_Complex -> (F_Real)-extending;
  coherence by RING_3:43,RING_3:48;
end;

registration
  cluster F_Real -> (F_Rat)-extending;
  coherence by RING_3:43,GAUSSINT:14;
end;

registration
  cluster F_Rat -> (INT.Ring)-extending;
  coherence by RING_3:47;
end;

registration
  let R be Ring, S be RingExtension of R;
  cluster -> R-extending for RingExtension of S;
  coherence
  proof
    let T be RingExtension of S;
    S is Subring of T & R is Subring of S by Def1;
    hence thesis by ALGNUM_1:1;
  end;
end;

registration
  let R be comRing, S be comRingExtension of R;
  cluster -> R-extending for comRingExtension of S;
  coherence;
end;

registration
  let R be domRing, S be domRingExtension of R;
  cluster -> R-extending for domRingExtension of S;
  coherence;
end;

registration
  let F be Field, E be FieldExtension of F;
  cluster -> F-extending for FieldExtension of E;
  coherence;
end;

registration
  let R be non degenerated Ring;
  cluster -> non degenerated for RingExtension of R;
  coherence
  proof
    let S be RingExtension of R;
A1: R is Subring of S by Def1;
    now assume S is degenerated; then
      1.R = 0.S by A1,C0SP1:def 3 .= 0.R by A1,C0SP1:def 3;
      hence contradiction;
    end;
    hence thesis;
  end;
end;

begin :: Extensions of Polynomial Rings

theorem Th5:
   for S being RingExtension of R, p being Polynomial of R holds
   p is Polynomial of S
   proof
     let S be RingExtension of R, p be Polynomial of R;
A1:  R is Subring of S by Def1; then
A2:  the carrier of R c= the carrier of S by C0SP1:def 3;
A3:  0.S = 0.R by A1,C0SP1:def 3;
     rng p c= the carrier of R by RELAT_1:def 19; then
     rng p c= the carrier of S by A2; then
     reconsider p1 = p as sequence of (the carrier of S) by FUNCT_2:6;
A4:  Support p is finite by POLYNOM1:def 5;
     now let o be object;
       assume
A5:    o in Support p1; then
       reconsider n = o as Element of NAT;
A6:    0.R <> p.n by A3,A5,POLYNOM1:def 3;
       dom p = NAT by FUNCT_2:def 1;
       hence o in Support p by A6,POLYNOM1:def 3;
     end; then
     Support p1 c= Support p;
     hence thesis by A4,POLYNOM1:def 5;
   end;

theorem
   for R being Subring of S, p being Polynomial of R holds
   p is Polynomial of S
   proof
     let R be Subring of S, p be Polynomial of R;
A2:  the carrier of R c= the carrier of S by C0SP1:def 3;
A3:  0.S = 0.R by C0SP1:def 3;
     rng p c= the carrier of R by RELAT_1:def 19; then
     rng p c= the carrier of S by A2; then
     reconsider p1 = p as sequence of (the carrier of S) by FUNCT_2:6;
A4:  Support p is finite by POLYNOM1:def 5;
     now let o be object;
       assume
A5:    o in Support p1; then
       reconsider n = o as Element of NAT;
A6:    0.R <> p.n by A3,A5,POLYNOM1:def 3;
       dom p = NAT by FUNCT_2:def 1;
       hence o in Support p by A6,POLYNOM1:def 3;
     end; then
     Support p1 c= Support p;
     hence thesis by A4,POLYNOM1:def 5;
   end;

theorem Th6:
   for S being RingExtension of R holds
   the carrier of Polynom-Ring R c= the carrier of Polynom-Ring S
   proof
     let S be RingExtension of R;
     now let o be object;
       assume o in the carrier of Polynom-Ring R; then
       o is Polynomial of R by POLYNOM3:def 10; then
       o is Polynomial of S by Th5;
       hence o in the carrier of Polynom-Ring S by POLYNOM3:def 10;
    end;
    hence thesis;
  end;

theorem Th7:
   S is RingExtension of R implies 0.(Polynom-Ring S) = 0.(Polynom-Ring R)
   proof
     assume S is R-extending Ring; then
A1:  R is Subring of S by Def1;
     thus
     0.(Polynom-Ring R) = 0_.(R) by POLYNOM3:def 10
     .= NAT --> 0.R by POLYNOM3:def 7
     .= NAT --> 0.S by A1,C0SP1:def 3
     .= 0_.(S) by POLYNOM3:def 7
     .= 0.(Polynom-Ring S) by POLYNOM3:def 10;
   end;

theorem Th8:
   S is RingExtension of R implies 0_.(S) = 0_.(R)
   proof
     assume
A1:  S is R-extending Ring;
     thus 0_.(S) = 0.(Polynom-Ring S) by POLYNOM3:def 10
     .= 0.(Polynom-Ring R) by A1,Th7
     .= 0_.(R) by POLYNOM3:def 10;
   end;

theorem Th9:
   S is RingExtension of R implies 1.(Polynom-Ring S) = 1.(Polynom-Ring R)
   proof
     assume
A1:  S is R-extending Ring; then
A2:  R is Subring of S by Def1;
     thus 1.(Polynom-Ring R) = 1_.(R) by POLYNOM3:def 10
     .= 0_.(R)+*(0,1.R) by POLYNOM3:def 8
     .= 0_.(R)+*(0,1.S) by A2,C0SP1:def 3
     .= 0_.(S)+*(0,1.S) by A1,Th8
     .= 1_.(S) by POLYNOM3:def 8
     .= 1.(Polynom-Ring S) by POLYNOM3:def 10;
   end;

theorem
   for S being RingExtension of R holds 1_.(S) = 1_.(R)
   proof
     let S be R-extending Ring;
     thus
     1_.(S) = 1.(Polynom-Ring S) by POLYNOM3:def 10
     .= 1.(Polynom-Ring R) by Th9
     .= 1_.(R) by POLYNOM3:def 10;
  end;

theorem Th10:
   for S being RingExtension of R, p,q being Polynomial of R
   for p1,q1 being Polynomial of S st p = p1 & q = q1 holds p + q = p1 + q1
   proof
     let S be RingExtension of R, p,q be Polynomial of R;
     let p1,q2 be Polynomial of S;
     assume
A1:  p = p1 & q = q2;
A2:  R is Subring of S by Def1;
     now let n be Element of NAT;
       p.n = p1.n & q.n = q2.n by A1; then
A3:    [p1.n,q2.n] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
       thus (p+q).n = p.n + q.n by NORMSP_1:def 2
       .= ((the addF of S)||the carrier of R).(p1.n,q2.n) by A1,A2,C0SP1:def 3
       .= p1.n + q2.n by A3,FUNCT_1:49
       .= (p1+q2).n by NORMSP_1:def 2;
     end;
     hence thesis;
   end;

theorem Th11:
   for S being RingExtension of R holds
   the addF of Polynom-Ring R
   = (the addF of Polynom-Ring S)||the carrier of Polynom-Ring R
   proof
     let S be RingExtension of R;
     set aR = the addF of Polynom-Ring R,
     aS = (the addF of Polynom-Ring S)||the carrier of Polynom-Ring R;
     set cR = the carrier of Polynom-Ring R,
     cS = the carrier of Polynom-Ring S;
A1:  cR c= cS by Th6;
A2:  dom aS = dom(the addF of Polynom-Ring S) /\ [:cR,cR:] by RELAT_1:61
     .= [:cS,cS:] /\ [:cR,cR:] by FUNCT_2:def 1
     .= [:cR,cR:] by A1,ZFMISC_1:96,XBOOLE_1:28
     .= dom aR by FUNCT_2:def 1;
     now let o be object;
       assume
A3:    o in dom aR; then
       consider p,q being object such that
A4:    p in the carrier of Polynom-Ring R &
       q in the carrier of Polynom-Ring R & o = [p,q] by ZFMISC_1:def 2;
       reconsider p,q as Element of cR by A4;
       reconsider p1 = p, q1 = q as Element of cS by A1;
       reconsider p2 = p, q2 = q as Polynomial of R;
       reconsider p3 = p1, q3 = q1 as Polynomial of S;
       thus
       aR.o = p + q by A4
       .= p2 + q2 by POLYNOM3:def 10
       .= p3 + q3 by Th10
       .= p1 + q1 by POLYNOM3:def 10
       .= aS.o by A2,A3,A4,FUNCT_1:47;
     end;
     hence thesis by A2;
   end;

theorem Th12:
   for S being RingExtension of R
   for p,q being Polynomial of R
   for p1,q1 being Polynomial of S st p = p1 & q = q1 holds p *' q = p1 *' q1
   proof
     let S be RingExtension of R;
     let p,q be Polynomial of R; let p1,q2 be Polynomial of S;
     assume
A1:  p = p1 & q = q2;
A2:  R is Subring of S by Def1;
     now let n be Element of NAT;
       consider r being FinSequence of the carrier of R such that
A3:    len r = n+1 & (p*'q).n = Sum r &
       for k being Element of NAT st k in dom r
       holds r.k = p.(k-'1) * q.(n+1-'k) by POLYNOM3:def 9;
       consider r1 being FinSequence of the carrier of S such that
A4:    len r1 = n+1 & (p1*'q2).n = Sum r1 &
       for k being Element of NAT st k in dom r1
       holds r1.k = p1.(k-'1) * q2.(n+1-'k) by POLYNOM3:def 9;
A5:    dom r1 = Seg(len r) by A3,A4,FINSEQ_1:def 3
       .= dom r by FINSEQ_1:def 3;
       now let m be Nat;
         assume
A6:      m in dom r;
         p.(m-'1) = p1.(m-'1) & q.(n+1-'m) = q2.(n+1-'m) by A1; then
A7:      [p1.(m-'1),q2.(n+1-'m)] in [:the carrier of R,the carrier of R:]
         by ZFMISC_1:def 2;
         thus
         r.m = p.(m-'1) * q.(n+1-'m) by A6,A3
         .= ((the multF of S)||the carrier of R).(p1.(m-'1),q2.(n+1-'m))
            by A1,A2,C0SP1:def 3
         .= p1.(m-'1) * q2.(n+1-'m) by A7,FUNCT_1:49
         .= r1.m by A6,A5,A4;
       end; then
       r = r1 by A5;
       hence (p*'q).n = (p1*'q2).n by A4,A3,A2,Th2;
     end;
     hence thesis;
   end;

theorem Th13:
   S is RingExtension of R implies  the multF of Polynom-Ring R
   = (the multF of Polynom-Ring S)||the carrier of Polynom-Ring R
   proof
     assume
AS:  S is RingExtension of R;
     set mR = the multF of Polynom-Ring R,
     mS = (the multF of Polynom-Ring S)||the carrier of Polynom-Ring R;
     set cR = the carrier of Polynom-Ring R,
     cS = the carrier of Polynom-Ring S;
A1:  cR c= cS by AS,Th6;
A2:  dom mS = dom(the multF of Polynom-Ring S) /\ [:cR,cR:] by RELAT_1:61
     .= [:cS,cS:] /\ [:cR,cR:] by FUNCT_2:def 1
     .= [:cR,cR:] by A1,ZFMISC_1:96,XBOOLE_1:28
     .= dom mR by FUNCT_2:def 1;
     now let o be object;
       assume
A3:    o in dom mR; then
       consider p,q being object such that
A4:    p in cR & q in cR & o = [p,q] by ZFMISC_1:def 2;
       reconsider p,q as Element of cR by A4;
       reconsider p1 = p, q1 = q as Element of cS by A1;
       reconsider p2 = p, q2 = q as Polynomial of R;
       reconsider p3 = p1, q3 = q1 as Polynomial of S;
       thus
       mR.o = p * q by A4
       .= p2 *' q2 by POLYNOM3:def 10
       .= p3 *' q3 by AS,Th12
       .= p1 * q1 by POLYNOM3:def 10
       .= mS.o by A4,A2,A3,FUNCT_1:47;
     end;
     hence thesis by A2;
   end;

registration
let R be Ring;
let S be RingExtension of R;
  cluster Polynom-Ring S -> (Polynom-Ring R)-extending;
  coherence
  proof
    set PS = Polynom-Ring S, PR = Polynom-Ring R;
A1: the addF of PR = (the addF of PS)||the carrier of PR by Th11;
A2: the multF of PR = (the multF of PS)||the carrier of PR by Th13;
    1.PS = 1.PR & 0.PS = 0.PR by Th7,Th9;
    hence thesis by Th6,A1,A2,C0SP1:def 3;
  end;
end;

theorem
   for R being Ring, S being RingExtension of R
   holds Polynom-Ring S is RingExtension of Polynom-Ring R;

theorem
   for S being RingExtension of R,
   p being Element of the carrier of Polynom-Ring R,
   q being Element of the carrier of Polynom-Ring S st p = q
   holds deg p = deg q
   proof
     let S be RingExtension of R;
     let p be Element of the carrier of Polynom-Ring R,
     q be Element of the carrier of Polynom-Ring S;
     assume
A1:  p = q;
A2:  R is Subring of S by Def1;
     per cases;
       suppose q is zero; then
         len q = 0 by UPROOTS:17; then
A3:      deg q = 0 - 1 by HURWITZ:def 2; then
         q = 0_.(S) by HURWITZ:20
         .= 0.(Polynom-Ring S) by POLYNOM3:def 10
         .= 0.(Polynom-Ring R) by Th7
         .= 0_.(R) by POLYNOM3:def 10;
         hence deg p = deg q by A1,A3,HURWITZ:20;
       end;
       suppose
A4:      q is non zero; then
         len q > 0 by UPROOTS:17; then
A5:      len q -' 1 = len q - 1 by XREAL_0:def 2; then
         reconsider lenq = len q - 1 as Element of NAT;
A6:      now let i be Nat;
           assume i >= len q; then
           q.i = 0.S by ALGSEQ_1:8;
           hence p.i = 0.R by A1,A2,C0SP1:def 3;
         end;
         now let m be Nat;
           assume
A7:        m is_at_least_length_of p;
           now assume len q > m; then
           lenq + 1 > m; then
           lenq >= m by NAT_1:13; then
           p.(len q-'1) = 0.R by A5,A7,ALGSEQ_1:def 2; then
A8:        q.(len q-'1) = 0.S by A1,A2,C0SP1:def 3;
           0 + 1 < len q + 1 by A4,XREAL_1:8,UPROOTS:17; then
           len q >= 1 by NAT_1:13; then
           (len q-'1) + 1 = len q by XREAL_1:235;
           hence contradiction by A8,ALGSEQ_1:10;
         end;
         hence len q <= m;
       end; then
       len p = len q by A6,ALGSEQ_1:def 3,ALGSEQ_1:def 2;
       hence deg p = len q - 1 by HURWITZ:def 2 .= deg q by HURWITZ:def 2;
     end;
   end;

Lm2:
   for S being RingExtension of R, a being Element of R, b being Element of S
   st a = b holds -a = -b
   proof
     let S be RingExtension of R;
     let a be Element of R, b be Element of S;
     assume
A1:  a = b;
A2:  R is Subring of S by Def1; then
     the carrier of R c= the carrier of S by C0SP1:def 3; then
     reconsider x = -a as Element of S;
A3:  [a,-a] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
A4:  (the addF of S)||the carrier of R = the addF of R by A2,C0SP1:def 3;
     b + x = a + -a by A1,A4,A3,FUNCT_1:49
     .= 0.R by RLVECT_1:5
     .= 0.S by A2,C0SP1:def 3;
     hence thesis by RLVECT_1:def 10;
   end;

theorem
   for R being non degenerated Ring, S being RingExtension of R,
   a being Element of R, b being Element of S st a = b
   holds rpoly(1,a) = rpoly(1,b)
   proof
     let R be non degenerated Ring, S be RingExtension of R;
     let a be Element of R, b be Element of S;
     assume
A1:  a = b;
A2:  R is Subring of S by Def1;
A3:  the carrier of Polynom-Ring R c= the carrier of Polynom-Ring S by Th6;
     set q = rpoly(1,b);
     reconsider p = rpoly(1,a) as Element of the carrier
     of Polynom-Ring R by POLYNOM3:def 10;
     reconsider p as Element of the carrier of Polynom-Ring S by A3;
     reconsider p as Polynomial of S;
     len q > 0 by UPROOTS:17; then
A4:  len q -' 1 = len q - 1 by XREAL_0:def 2; then
     reconsider lenq = len q - 1 as Element of NAT;
A5:  1 = deg q by HURWITZ:27 .= len q - 1 by HURWITZ:def 2; then
A6:  len q = 1 + 1;
A7:   now let i be Nat;
       assume
A8:    i >= len q;
       reconsider j = i as Element of NAT by ORDINAL1:def 12;
       j <> 0 & j <> 1 by A8,A6; then
       rpoly(1,a).j = 0.R by HURWITZ:26;
       hence p.i = 0.S by A2,C0SP1:def 3;
     end;
     now let m be Nat;
       assume
A9:    m is_at_least_length_of p;
       reconsider j = lenq as Element of NAT;
       now assume len q > m; then
         lenq + 1 > m; then
         lenq >= m by NAT_1:13; then
A10:     p.(len q-'1) = 0.S by A4,A9,ALGSEQ_1:def 2;
         rpoly(1,a).1 = 1_R by HURWITZ:25 .= 1.S by A2,C0SP1:def 3;
         hence contradiction by A10,A5,XREAL_0:def 2;
       end;
       hence len q <= m;
     end; then
A11: len p = len q by A7,ALGSEQ_1:def 3,ALGSEQ_1:def 2;
     now let k be Nat;
       assume
A12:   k < len q;
       len q - 1 = deg q by HURWITZ:def 2 .= 1 by HURWITZ:27; then
       k < 1 + 1 by A12; then
A13:   k <= 1 by NAT_1:13;
       per cases;
         suppose
A14:       k = 0; then
A15:       rpoly(1,a).k = -power(R).(a,0+1) by HURWITZ:25
           .= -(power(R).(a,0) * a) by GROUP_1:def 7
           .= -(1_R * a) by GROUP_1:def 7
           .= -b by A1,Lm2;
           q.k = -power(S).(b,0+1) by A14,HURWITZ:25
           .= -(power(S).(b,0) * b) by GROUP_1:def 7
           .= -(1_S * b) by GROUP_1:def 7
           .= -b;
           hence p.k = q.k by A15;
         end;
         suppose k <> 0; then
           k + 1 > 0 + 1 by XREAL_1:6; then
A16:       k >= 1 by NAT_1:13; then
A17:       k = 1 by A13,XXREAL_0:1;
           rpoly(1,a).1 = 1_R by HURWITZ:25 .= 1.S by A2,C0SP1:def 3;
           hence p.k = 1_S by A16,A13,XXREAL_0:1 .= q.k by
           A17,HURWITZ:25;
         end;
       end;
       hence thesis by A11,ALGSEQ_1:12;
     end;

begin :: Evaluation of Polynomials in Ring Extensions

theorem
   for a be Element of S holds
   S is RingExtension of R implies Ext_eval(0_.(R),a) = 0.S by ALGNUM_1:13;

theorem
   for R being non degenerated Ring, S being RingExtension of R,
   a being Element of S holds Ext_eval(1_.(R),a) = 1.S
   proof
     let R be non degenerated Ring, S be RingExtension of R;
     let a be Element of S;
     R is Subring of S by Def1;
     hence thesis by ALGNUM_1:14;
   end;

theorem
   for S being RingExtension of R,a being Element of S,
   p,q being Polynomial of R holds
   Ext_eval(p+q,a) = Ext_eval(p,a) + Ext_eval(q,a)
   proof
     let S be RingExtension of R, a be Element of S;
     let p,q be Polynomial of R;
     R is Subring of S by Def1;
     hence thesis by ALGNUM_1:15;
   end;

theorem
   for R being comRing, S being comRingExtension of R, a being Element of S,
   p,q being Polynomial of R holds
   Ext_eval(p*'q,a) = Ext_eval(p,a) * Ext_eval(q,a)
   proof
     let R be comRing, S be comRingExtension of R;
     let a be Element of S;
     let p,q be Polynomial of R;
     R is Subring of S by Def1;
     hence thesis by ALGNUM_1:20;
  end;

Th14:
   for S being RingExtension of R,
   p being Element of the carrier of Polynom-Ring R,
   a being Element of R, b being Element of S st b = a holds
   Ext_eval(p,b) = eval(p,a)
   proof
     let S be RingExtension of R;
     let p be Element of the carrier of Polynom-Ring R;
     let a be Element of R, b be Element of S;
     assume
A1:  b = a;
A2:  R is Subring of S by Def1; then
A3:  the carrier of R c= the carrier of S by C0SP1:def 3;
     Ext_eval(p,In(a,S)) = In(eval(p,a),S) by A2,ALGNUM_1:12
     .= eval(p,a) by A3,SUBSET_1:def 8;
     hence thesis by A1;
   end;

theorem Th15:
   for S being RingExtension of R,
   p being Element of the carrier of (Polynom-Ring R),
   q being Element of the carrier of Polynom-Ring S,
   a being Element of S st p = q holds Ext_eval(p,a) = eval(q,a)
   proof
     let S be RingExtension of R;
     let p be Element of the carrier of (Polynom-Ring R),
     q be Element of the carrier of Polynom-Ring S;
     let a be Element of S;
     assume
A1:  p = q;
A2:  R is Subring of S by Def1;
     per cases;
       suppose q is zero; then
A3:      q = 0_.(S) by UPROOTS:def 5;
         p = 0.(Polynom-Ring S) by A1,A3,POLYNOM3:def 10
         .= 0.(Polynom-Ring R) by Th7
         .= 0_.(R) by POLYNOM3:def 10;
         hence
         Ext_eval(p,a) = 0.S by ALGNUM_1:13 .= eval(q,a) by A3,POLYNOM4:17;
       end;
      suppose
A4:     q is non zero; then
        len q > 0 by UPROOTS:17; then
A5:     len q -' 1 = len q - 1 by XREAL_0:def 2; then
        reconsider lenq = len q - 1 as Element of NAT;
        consider Fp being FinSequence of S such that
A6:     Ext_eval(p,a) = Sum Fp & len Fp = len p &
        for n being Element of NAT st n in dom Fp holds
        Fp.n = In(p.(n-'1),S) * (power S).(a,n-'1) by ALGNUM_1:def 1;
        consider Fq being FinSequence of the carrier of S such that
A7:     eval(q,a) = Sum Fq & len Fq = len q &
        for n being Element of NAT st n in dom Fq holds
        Fq.n = q.(n-'1) * (power S).(a,n-'1) by POLYNOM4:def 2;
A8:     now let i be Nat;
          assume i >= len q; then
          q.i = 0.S by ALGSEQ_1:8;
          hence p.i = 0.R by A1,A2,C0SP1:def 3;
        end;
        now let m be Nat;
          assume
A9:       m is_at_least_length_of p;
          now assume len q > m; then
          lenq + 1 > m; then
          lenq >= m by NAT_1:13; then
          p.(len q-'1) = 0.R by A5,A9,ALGSEQ_1:def 2; then
A10:       q.(len q-'1) = 0.S by A1,A2,C0SP1:def 3;
          0 + 1 < len q + 1 by A4,XREAL_1:8,UPROOTS:17; then
          len q >= 1 by NAT_1:13; then
          (len q-'1) + 1 = len q by XREAL_1:235;
          hence contradiction by A10,ALGSEQ_1:10;
        end;
        hence len q <= m;
      end; then
      len p = len q by A8,ALGSEQ_1:def 3,ALGSEQ_1:def 2; then
A11:  dom Fq = Seg(len p) by A7,FINSEQ_1:def 3
      .= dom Fp by A6,FINSEQ_1:def 3;
      for n being Nat st n in dom Fp holds Fq.n = Fp.n
      proof
        let n be Nat;
        assume
A12:    n in dom Fp;
        hence Fp.n = In(p.(n-'1),S) * (power S).(a,n-'1) by A6
        .= q.(n-'1) * (power S).(a,n-'1) by A1
        .= Fq.n by A7,A11,A12;
      end;
      hence thesis by A6,A7,A11,FINSEQ_1:13;
    end;
  end;

theorem
   for S being RingExtension of R,
   p being Element of the carrier of (Polynom-Ring R),
   q being Element of the carrier of Polynom-Ring S,
   a being Element of R, b being Element of S st q = p & b = a
   holds eval(q,b) = eval(p,a)
   proof
     let S be RingExtension of R,
     p be Element of the carrier of (Polynom-Ring R),
     q be Element of the carrier of Polynom-Ring S,
     a being Element of R, b being Element of S;
     assume that
A1:  p = q and
A2:  a = b;
     thus eval(p,a) = Ext_eval(p,b) by A2,Th14 .= eval(q,b) by A1,Th15;
   end;

definition
  let R be Ring, S be RingExtension of R;
  let p be Element of the carrier of Polynom-Ring R;
  let a be Element of S;
  pred a is_a_root_of p,S means
  Ext_eval(p,a) = 0.S;
end;

definition
  let R be Ring, S be RingExtension of R;
  let p be Element of the carrier of Polynom-Ring R;
  pred p is_with_roots_in S means
  ex a being Element of S st a is_a_root_of p,S;
end;

definition
  let R be Ring, S be RingExtension of R;
  let p be Element of the carrier of Polynom-Ring R;
  func Roots(S,p) -> Subset of S equals
  {a where a is Element of S : a is_a_root_of p,S};
  coherence
  proof
    now let o be object;
      assume o in {a where a is Element of S : a is_a_root_of p,S}; then
      consider a being Element of S such that
A1:   o = a & a is_a_root_of p,S;
      thus o in the carrier of S by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem
   for S being RingExtension of R,
   p being Element of the carrier of Polynom-Ring R
   holds Roots p c= Roots(S,p)
   proof
     let S be RingExtension of R;
     let p be Element of the carrier of Polynom-Ring R;
A1:  R is Subring of S by Def1; then
A2:  the carrier of R c= the carrier of S by C0SP1:def 3;
     now let o be object;
       assume
A3:    o in Roots p; then
       reconsider a = o as Element of R;
A4:    a is_a_root_of p by A3,POLYNOM5:def 10;
       reconsider b = a as Element of S by A2;
       Ext_eval(p,b) = eval(p,a) by Th14
       .= 0.R by A4,POLYNOM5:def 7
       .= 0.S by A1,C0SP1:def 3; then
       b is_a_root_of p,S;
       hence o in Roots(S,p);
     end;
     hence thesis;
   end;

::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
definition
  let R be Ring, S be non degenerated Ring;
  let p be Polynomial of R;
  pred p splits_in S means
  ex a being non zero Element of S, q being Ppoly of S st p = a * q;
end;

::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
theorem
   for F being Field, p be Polynomial of F st deg p = 1 holds p splits_in F
   proof
     let F be Field;
     let p be Polynomial of F;
     assume deg p = 1; then
     consider x,z being Element of F such that
A1:  x <> 0.F & p = x * rpoly(1,z) by HURWITZ:28;
     reconsider x as non zero Element of F by A1,STRUCT_0:def 12;
     reconsider q = rpoly(1,z) as Ppoly of F by RING_5:51;
     p = x * q by A1;
     hence thesis;
   end;

begin :: Degree of Extension

definition
  let R be Ring, S be RingExtension of R;
  func VecSp(S,R) -> strict ModuleStr over R means
:Def5:
  the carrier of it = the carrier of S &
  the addF of it = the addF of S &
  the ZeroF of it = 0.S &
  the lmult of it = (the multF of S)|[:the carrier of R,the carrier of S:];
  existence
  proof
    set C = the carrier of S;
    R is Subring of S by Def1; then
    the carrier of R c= C by C0SP1:def 3; then
    [:the carrier of R,C:] c= [:C,C:] by ZFMISC_1:96; then
    reconsider lm = (the multF of S)|[:the carrier of R,C:]
    as Function of [:the carrier of R,C:],C by FUNCT_2:32;
    take ModuleStr (# C,the addF of S,0.S,lm #);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let R be Ring, S be RingExtension of R;
  cluster VecSp(S,R) -> non empty;
  coherence
  proof
    0.S in the carrier of S;
    hence thesis by Def5;
  end;
end;

registration
  let R be Ring, S be RingExtension of R;
  cluster VecSp(S,R) ->
  Abelian add-associative right_zeroed right_complementable;
  coherence
  proof
    set E = S, F = R; set P = VecSp(E,F);
A1: 0.P = 0.E by Def5;
    hereby
      let x,y be Element of P;
      reconsider a = x, b = y as Element of E by Def5;
      thus
      x+y = a+b by Def5 .= b+a by RLVECT_1:def 2 .= y+x by Def5;
    end;
    hereby
      let x,y,z be Element of P;
      reconsider a = x, b = y, c = z as Element of E by Def5;
A2:   y+z = b+c by Def5;
      x+y = a+b by Def5;
      hence x+y+z = a+b+c by Def5
      .= a+(b+c) by RLVECT_1:def 3
      .= x+(y+z) by A2,Def5;
    end;
    hereby
      let x be Element of P;
      reconsider a = x as Element of E by Def5;
      thus x+0.P = a+0.E by A1,Def5 .= x;
    end;
    let x be Element of P;
    reconsider a = x as Element of E by Def5;
    consider b being Element of E such that
A3: a + b = 0.E by ALGSTR_0:def 11;
    reconsider y = b as Element of P by Def5;
    take y;
    thus x+y = a+b by Def5 .= 0.P by A3,Def5;
  end;
end;

Lm3:
   for E be RingExtension of R, a,b be Element of E, s be Element of R,
   v be Element of VecSp(E,R) st a = s & b = v holds a*b = s*v
   proof
     let E be RingExtension of R;
     let a,b be Element of E;
     let s be Element of R, v be Element of VecSp(E,R) such that
A1:  a = s & b = v;
     the carrier of VecSp(E,R) = the carrier of E by Def5; then
A2:  [s,v] in [:the carrier of R,the carrier of E:] by ZFMISC_1:def 2;
     thus
     s * v
      = ((the multF of E)|[:the carrier of R,the carrier of E:]).(s,v) by Def5
     .= a*b by A1,A2,FUNCT_1:49;
   end;

Lm4:
   for E be RingExtension of R, a,b be Element of E, x,y be Element of R
   st a = x & b = y holds a+b = x+y
   proof
     let E be RingExtension of R;
     let a,b be Element of E;
     let x,y be Element of R such that
A1:  a = x & b = y;
A2:  R is Subring of E by Def1;
A3:  [x,y] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
     thus
     x+y = ((the addF of E)||(the carrier of R)).(x,y) by A2,C0SP1:def 3
     .= a+b by A1,A3,FUNCT_1:49;
   end;

Lm5:
   for E be RingExtension of R, a,b be Element of E, x,y be Element of R
   st a = x & b = y holds a*b = x*y
   proof
     let E be RingExtension of R;
     let a,b be Element of E;
     let x,y be Element of R such that
A1:  a = x & b = y;
A2:  R is Subring of E by Def1;
A3:  [x,y] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
     thus
     x*y = ((the multF of E)||(the carrier of R)).(x,y) by A2,C0SP1:def 3
     .= a*b by A1,A3,FUNCT_1:49;
   end;

registration
  let R be Ring, S be RingExtension of R;
  cluster VecSp(S,R) ->
  scalar-distributive scalar-associative scalar-unital vector-distributive;
  coherence
  proof
    set E = S, F = R; set P = VecSp(E,F);
A1: F is Subring of E by Def1; then
A2: the carrier of F c= the carrier of E by C0SP1:def 3;
    hereby
      let x,y be Element of F;
      let v be Element of P;
      reconsider a = x, b = y, c = v as Element of E by A2,Def5;
A3:   (a+b)*c = a*c+b*c by VECTSP_1:def 3;
      x*v = a*c & y*v = b*c by Lm3; then
      x*v+y*v = a*c + b*c by Def5;
      hence (x+y)*v = x*v+y*v by A3,Lm3,Lm4;
    end;
    hereby
      let x,y be Element of F;
      let v be Element of P;
      reconsider a = x, b = y, c = v as Element of E by A2,Def5;
A4:   (a*b)*c = a*(b*c) by GROUP_1:def 3;
A5:   (a*b)*c = (x*y)*v by Lm3,Lm5;
      b*c = y*v by Lm3;
      hence (x*y) * v = x * (y*v) by A4,A5,Lm3;
    end;
    hereby
      let v be Element of P;
      reconsider c = v as Element of E by Def5;
A6:   1.F = 1.E by C0SP1:def 3,A1;
      (1.E) * c = c;
      hence (1.F) * v = v by Lm3,A6;
    end;
    hereby
      let x be Element of F;
      let v,w be Element of P;
      reconsider a = x, b = v, c = w as Element of E by A2,Def5;
A7:   a*(b+c) = a*b+a*c by VECTSP_1:def 2;
      b+c = v+w by Def5; then
A8:   a*(b+c) = x*(v+w) by Lm3;
      a*b = x*v & a*c = x*w by Lm3;
      hence x*(v+w) = x*v+x*w by A7,A8,Def5;
    end;
  end;
end;

theorem
  for S being RingExtension of R holds VecSp(S,R) is VectSp of R;

definition
  let F be Field, E be FieldExtension of F;
  func deg(E,F) -> Integer equals
:Def6:
  dim VecSp(E,F) if VecSp(E,F) is finite-dimensional
  otherwise -1;
  coherence;
  consistency;
end;

registration
  let F be Field, E be FieldExtension of F;
  cluster deg(E,F) -> dim-like;
  coherence
  proof
    now assume
A1:   not deg(E,F) = -1;
      dim VecSp(E,F) is Nat;
      hence deg(E,F) is natural by Def6,A1;
    end;
    hence thesis;
  end;
end;

definition
let F be Field, E be FieldExtension of F;
  attr E is F-finite means
:Def7:
  VecSp(E,F) is finite-dimensional;
end;

registration
  let F be Field;
  cluster F-finite for FieldExtension of F;
  existence
  proof
    reconsider E = F as FieldExtension of F by Th3;
    take E;
    set V = VecSp(E,F);
A1: the carrier of V = the carrier of E by Def5;
    reconsider e = 1.E as Vector of V by Def5;
    for x be object st x in {1.E} holds x in the carrier of V by A1; then
    reconsider A = {e} as Subset of V by TARSKI:def 3;
    0.V = 0.E by Def5; then
A2: A is linearly-independent by VECTSP_7:3;
A3: the carrier of Lin(A) =
    the set of all Sum(l) where l is Linear_Combination of A by VECTSP_7:def 2;
A4: now let o be object;
    assume o in the carrier of V; then
    reconsider v = o as Element of the carrier of V;
    reconsider a = v as Element of E by Def5;
    defpred P[object,object] means
    ($1 = e & $2 = a) or ($1 <> e & $2 = 0.E);
A6: for x being object st x in the carrier of V
    ex y being object st y in the carrier of E & P[x,y]
      proof
        let o be object;
        assume o in the carrier of V;
        per cases;
          suppose
A7:         o = e;
            take a;
            thus thesis by A7;
          end;
          suppose
A8:         o <> e;
            take 0.E;
            thus thesis by A8;
          end;
        end;
        consider f being Function of the carrier of V, the carrier of E
        such that
A9:     for x being object st x in the carrier of V holds P[x,f.x]
        from FUNCT_2:sch 1(A6);
        dom f = the carrier of V & rng f c= the carrier of E
        by RELAT_1:def 19,FUNCT_2:def 1; then
        reconsider f as Element of Funcs(the carrier of V, the carrier of E)
        by FUNCT_2:def 2;
        ex T being finite Subset of V st
        for v being Element of V st not v in T holds f.v = 0.E
        proof
          e in the carrier of V; then
          for x be object holds x in {e} implies x in the carrier of V
          by TARSKI:def 1; then
          reconsider T = {e} as finite Subset of V by TARSKI:def 3;
          take T;
          now let u be Element of V;
          assume not u in T; then
          u <> e by TARSKI:def 1;
          hence f.u = 0.E by A9;
        end;
      hence thesis;
      end; then
      reconsider l = f as Linear_Combination of V by VECTSP_6:def 1;
      now let o be object;
        assume o in Carrier l; then
        o in {v where v is Element of V: l.v <> 0.E} by VECTSP_6:def 2; then
        consider u being Element of V such that
A10:    o = u & l.u <> 0.E;
        u = e by A10,A9;
        hence o in A by A10,TARSKI:def 1;
      end; then
      Carrier l c= A; then
      reconsider l as Linear_Combination of A by VECTSP_6:def 4;
      Sum l = l.e * e by VECTSP_6:17
      .= ((the multF of E)|[:the carrier of F,the carrier of E:]).(l.e,e)
      by Def5
      .= a * 1.E by A9
      .= v;
      hence o in the set of all Sum(l) where l is Linear_Combination of A;
    end;
    now let o be object;
      assume o in the set of all Sum(l) where l is Linear_Combination of A;
      then
      consider l being Linear_Combination of A such that
A11:  o = Sum l;
      thus o in the carrier of V by A11;
    end; then
    the carrier of V = the set of all Sum(l) where
    l is Linear_Combination of A by A4,TARSKI:2; then
    A is Basis of V by A3,A2,VECTSP_4:31,VECTSP_7:def 3;
    hence thesis by MATRLIN:def 1;
  end;
end;

registration
  let F be Field;
  let E be F-finite FieldExtension of F;
  cluster deg(E,F) -> natural;
  coherence
  proof
    dim VecSp(E,F) is Nat;
    hence deg(E,F) is natural by Def7,Def6;
  end;
end;

begin :: Kronecker's Theorem

registration
  let F be Field, p be non constant Element of the carrier of Polynom-Ring F;
  cluster the carrier of (Polynom-Ring p) -> F-polynomial-membered;
  coherence
  proof
A1: the carrier of (Polynom-Ring p) =
    {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
    now let o be object;
      assume o in the carrier of (Polynom-Ring p); then
      consider q being Polynomial of F such that
A2:   q = o & deg q < deg p by A1;
      thus
      o is Polynomial of F by A2;
    end;
    hence thesis;
  end;
  cluster Polynom-Ring p -> F-polynomial-membered;
  coherence;
end;

definition
  let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
  func KroneckerIso p ->
  Function of the carrier of Polynom-Ring p,the carrier of KroneckerField(F,p)
  means
:Def8:
  for q being Element of the carrier of Polynom-Ring p
  holds it.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q);
  existence
  proof
    deffunc F(object) = Class(EqRel(Polynom-Ring F,{p}-Ideal),$1);
A1: the carrier of Polynom-Ring p =
    {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
A2:  now let x be object;
      assume
A3:   x in the carrier of Polynom-Ring p;
      for a being Element of Polynom-Ring p
      holds a in the carrier of Polynom-Ring F
      proof
        let a be Element of Polynom-Ring p;
        a in {q where q is Polynomial of F : deg q < deg p} by A1; then
        ex r being Polynomial of F st r = a & deg r < deg p;
        hence thesis by POLYNOM3:def 10;
      end; then
      reconsider a = x as Element of Polynom-Ring F by A3;
      Class(EqRel(Polynom-Ring F,{p}-Ideal),a) is
      Element of (Polynom-Ring F)/({p}-Ideal) by RING_1:12; then
      Class(EqRel(Polynom-Ring F,{p}-Ideal),a) in
      the carrier of (Polynom-Ring F)/({p}-Ideal);
      hence F(x) in the carrier of KroneckerField(F,p) by FIELD_1:def 3;
    end;
    consider g being Function of the carrier of Polynom-Ring p,
    the carrier of KroneckerField(F,p) such that
A4:  for x being object st x in the carrier of Polynom-Ring p holds
    g.x = F(x) from FUNCT_2:sch 2(A2);
    take g;
    thus
    thesis by A4;
  end;
  uniqueness
  proof
    set R = Polynom-Ring p;
    let F1,F2 be Function of the carrier of Polynom-Ring p,
    the carrier of KroneckerField(F,p) such that
A5: for q being Element of R
    holds F1.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q) and
A6: for q being Element of R
    holds F2.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q);
    now let q be Element of R;
      thus
      F1.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q) by A5 .= F2.q by A6;
    end;
    hence thesis;
  end;
end;

Lm6:
  for L be Ring, a be Element of Polynom-Ring L, p be Polynomial of L
  st a = p holds - a = -p
  proof
    let L be Ring, a be Element of Polynom-Ring L, p be Polynomial of L;
    reconsider x = -p as Element of Polynom-Ring L by POLYNOM3:def 10;
    assume a = p; then
    a + x = p + -p by POLYNOM3:def 10
    .= p - p by POLYNOM3:def 6
    .= 0_.(L) by POLYNOM3:29
    .= 0.(Polynom-Ring(L)) by POLYNOM3:def 10; then
    a = - x by RLVECT_1:6;
    hence - a = -p;
  end;

Lm7:
    for L be Ring, a,b be Element of Polynom-Ring L, p,q be Polynomial of L
    st a = p & b = q holds a -b = p - q
    proof
      let L be Ring, a,b be Element of Polynom-Ring L, p,q be Polynomial of L;
      assume
A1:   a = p & b = q; then
      -b = -q by Lm6;
      hence a - b = p + (-q) by A1,POLYNOM3:def 10
      .= p - q by POLYNOM3:def 6;
    end;

Lm8:
   for F be Field, p be irreducible Element of the carrier of Polynom-Ring F,
   a be Element of Polynom-Ring p holds
   a in the carrier of Polynom-Ring F
   proof
     let F be Field,
     p be irreducible Element of the carrier of Polynom-Ring F,
     a be Element of Polynom-Ring p;
     the carrier of Polynom-Ring p
     = {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8; then
     a in {q where q is Polynomial of F : deg q < deg p}; then
     ex r being Polynomial of F st r = a & deg r < deg p;
     hence a in the carrier of Polynom-Ring F by POLYNOM3:def 10;
   end;

Lm9:
   for F be Field,
   p be irreducible Element of the carrier of Polynom-Ring F,
   a be Element of the carrier of Polynom-Ring F,
   q be Element of Polynom-Ring p st a = q
   holds - a = -q
   proof
     let F be Field,
     p be irreducible Element of the carrier of Polynom-Ring F,
     a be Element of the carrier of Polynom-Ring F,
     q be Element of Polynom-Ring p;
     reconsider x = -q as Element of Polynom-Ring F by Lm8;
A1:  the addF of Polynom-Ring p
     = (the addF of Polynom-Ring F)||(the carrier of Polynom-Ring p)
     by RING_4:def 8;
A2:  the ZeroF of Polynom-Ring p = 0_.(F) by RING_4:def 8;
     assume
A3:  a = q;
     [a,x] in [:the carrier of Polynom-Ring p,
     the carrier of Polynom-Ring p:] by A3,ZFMISC_1:def 2; then
     a + x = q + -q by A3,A1,FUNCT_1:49
     .= 0.(Polynom-Ring p) by RLVECT_1:5
     .= 0.(Polynom-Ring(F)) by A2,POLYNOM3:def 10; then
     a = - x by RLVECT_1:6;
     hence - a = -q;
   end;

Lm10:
   for F be Field, p be irreducible Element of the carrier of Polynom-Ring F,
   a,b be Element of the carrier of Polynom-Ring F,
   q,r be Element of Polynom-Ring p st a = q & b = r holds a - b = q - r
   proof
     let F be Field, p be irreducible Element of the carrier of Polynom-Ring F,
     a,b be Element of the carrier of Polynom-Ring F,
     q,r be Element of Polynom-Ring p;
     assume
A1:  a = q & b = r; then
     -b = -r by Lm9; then
A2:  [a,-b] in [:the carrier of Polynom-Ring p,
     the carrier of Polynom-Ring p:] by A1,ZFMISC_1:def 2;
A3:  the addF of Polynom-Ring p
     = (the addF of Polynom-Ring F)||(the carrier of Polynom-Ring p)
     by RING_4:def 8;
     a - b = (the addF of Polynom-Ring p).(a,-b) by A2,A3,FUNCT_1:49
     .= q - r by A1,Lm9;
     hence thesis;
   end;

registration
  let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
  cluster KroneckerIso p ->
  additive multiplicative unity-preserving one-to-one onto;
  coherence
  proof
    set R = Polynom-Ring p, f = KroneckerIso p;
    now let a,b be Element of R;
      reconsider r = a, q = b as Element of Polynom-Ring F by Lm8;
      reconsider fa = f.a, fb = f.b as Element of (Polynom-Ring F)/({p}-Ideal)
      by FIELD_1:def 3;
A1:   fa = Class(EqRel(Polynom-Ring F,{p}-Ideal),a) by Def8;
A2:   fb = Class(EqRel(Polynom-Ring F,{p}-Ideal),b) by Def8;
A3:   [a,b] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
A4:   a + b = ((the addF of Polynom-Ring F)||(the carrier of R)).(a,b)
      by RING_4:def 8
      .= r + q by A3,FUNCT_1:49;
      thus f.a + f.b = fa + fb by FIELD_1:def 3
      .= Class(EqRel(Polynom-Ring F,{p}-Ideal),a+b) by A4,A1,A2,RING_1:13
      .= f.(a+b) by Def8;
    end;
    hence f is additive;
    now let a,b be Element of R;
      reconsider r = a, q = b as Element of the carrier of Polynom-Ring F
      by Lm8;
      reconsider fa = f.a, fb = f.b as Element of (Polynom-Ring F)/({p}-Ideal)
      by FIELD_1:def 3;
A5:   fa = Class(EqRel(Polynom-Ring F,{p}-Ideal),a) by Def8;
A6:   fb = Class(EqRel(Polynom-Ring F,{p}-Ideal),b) by Def8;
A7:   [a,b] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
A8:   a * b = (poly_mult_mod p)||(the carrier of R).(a,b) by RING_4:def 8
      .= (poly_mult_mod p).(r,q) by A7,FUNCT_1:49
      .= (r *' q) mod p by RING_4:def 7;
      reconsider c = (r *' q) mod p as Element of the carrier of Polynom-Ring F
      by POLYNOM3:def 10;
      reconsider d = (r *' q) div p as Element of the carrier of Polynom-Ring F
      by POLYNOM3:def 10;
A9:   (r *' q) - ((r *' q) mod p)
       = ((r *' q) div p) *' p + ((r *' q) mod p)-((r *' q) mod p) by RING_4:4
      .= (((r *' q) div p) *' p + ((r *' q) mod p)) + -((r *' q) mod p)
      by POLYNOM3:def 6
      .= ((r *' q) div p) *' p + (((r *' q) mod p) + -((r *' q) mod p))
      by POLYNOM3:26
      .= ((r *' q) div p) *' p + (((r *' q) mod p) - ((r *' q) mod p))
      by POLYNOM3:def 6
      .= ((r *' q) div p) *' p + 0_.(F) by POLYNOM3:29
      .= ((r *' q) div p) *' p;
      r * q = r *' q by POLYNOM3:def 10; then
A10:  r * q - c = ((r *' q) div p) *' p by A9,Lm7
      .= p * d by POLYNOM3:def 10;
      {p}-Ideal = the set of all p * r where r is Element of Polynom-Ring F
      by IDEAL_1:64; then
A11:  r*q - c in {p}-Ideal by A10;
      thus
      f.a * f.b = fa * fb by FIELD_1:def 3
      .= Class(EqRel(Polynom-Ring F,{p}-Ideal),r*q) by A5,A6,RING_1:14
      .= Class(EqRel(Polynom-Ring F,{p}-Ideal),a*b) by A11,A8,RING_1:6
      .= f.(a*b) by Def8;
      end;
      hence f is multiplicative;
      f.1_R = Class(EqRel(Polynom-Ring F,{p}-Ideal),1.R) by Def8
      .= Class(EqRel(Polynom-Ring F,{p}-Ideal),1_.(F)) by RING_4:def 8
      .= Class(EqRel(Polynom-Ring F,{p}-Ideal),1.(Polynom-Ring F))
         by POLYNOM3:def 10
      .= 1.((Polynom-Ring F)/({p}-Ideal)) by RING_1:def 6
      .= 1_KroneckerField(F,p) by FIELD_1:def 3;
      hence f is unity-preserving;
      now let x1,x2 be object;
        assume
A12:    x1 in dom f & x2 in dom f & f.x1 = f.x2; then
  reconsider a = x1, b = x2 as Element of the carrier of Polynom-Ring p;
  reconsider q = a, r = b as Element of the carrier of Polynom-Ring F by Lm8;
        Class(EqRel(Polynom-Ring F,{p}-Ideal),q) = f.b by A12,Def8
        .= Class(EqRel(Polynom-Ring F,{p}-Ideal),r) by Def8; then
        q - r in {p}-Ideal by RING_1:6; then
        q - r in the set of all p*s where s is Element of Polynom-Ring F
        by IDEAL_1:64; then
        consider u being Element of the carrier of Polynom-Ring F such that
A13:    q - r = p * u;
        reconsider s = p *'u as Polynomial of F;
A14:    q - r = a - b by Lm10;
        now assume
A15:      u <> 0_.(F); then
          reconsider degu = deg u as Element of NAT by FIELD_1:1;
          degu >= 0; then
A16:      deg p + deg u >= deg p + 0 by XREAL_1:6;
          now assume p *' u in {q where q is Polynomial of F : deg q < deg p};
          then
          consider s being Polynomial of F such that
A17:      s = p *' u & deg s < deg p;
          thus
          contradiction by A17,A16,A15,HURWITZ:23;
        end; then
        not p *' u in the carrier of Polynom-Ring p by RING_4:def 8; then
        not q - r in the carrier of Polynom-Ring p by A13,POLYNOM3:def 10;
        hence contradiction by A14;
      end; then
      q - r = p *' (0_.(F)) by A13,POLYNOM3:def 10
      .= 0.(Polynom-Ring F) by POLYNOM3:def 10;
      hence x1 = x2 by RLVECT_1:21;
    end;
    hence f is one-to-one;
A18:  now let x be object;
      assume
A19:  x in rng f;
      rng f c= the carrier of KroneckerField(F,p) by RELAT_1:def 19;
      hence x in the carrier of KroneckerField(F,p) by A19;
    end;
    now let x be object;
      assume x in the carrier of KroneckerField(F,p); then
      x in the carrier of (Polynom-Ring F)/({p}-Ideal) by FIELD_1:def 3; then
      consider q being Element of the carrier of Polynom-Ring F such that
A20:  x = Class(EqRel(Polynom-Ring F,{p}-Ideal),q) by RING_1:11;
      reconsider d = q div p as Element of the carrier of Polynom-Ring F
      by POLYNOM3:def 10;
      p <> 0_.(F); then
      consider t being Polynomial of F such that
A21:  q = (q div p) *' p + t & deg t < deg p by HURWITZ:def 5;
      reconsider r = t as Element of the carrier of Polynom-Ring F
      by POLYNOM3:def 10;
      q - (q div p) *' p
      = ((q div p) *' p + t) + -((q div p) *' p) by A21,POLYNOM3:def 6
      .= t + ((q div p) *' p + -((q div p) *' p)) by POLYNOM3:26
      .= t + ((q div p) *' p - ((q div p) *' p)) by POLYNOM3:def 6
      .= t + 0_.(F) by POLYNOM3:29
      .= t; then
A22:  r = q mod p by HURWITZ:def 6;
      r in {q where q is Polynomial of F : deg q < deg p} by A21; then
A23:  r in the carrier of Polynom-Ring p by RING_4:def 8; then
A24:  r in dom f by FUNCT_2:def 1;
      q = (q div p) *' p + (q mod p) by RING_4:4; then
A25:  q - r = ((q div p) *' p + (q mod p)) - (q mod p) by A22,Lm7
      .= ((q div p) *' p + (q mod p)) + -(q mod p) by POLYNOM3:def 6
      .= (q div p) *' p + ((q mod p) + -(q mod p)) by POLYNOM3:26
      .= (q div p) *' p + ((q mod p) - (q mod p)) by POLYNOM3:def 6
      .= (q div p) *' p + 0_.(F) by POLYNOM3:29
      .= p * d by POLYNOM3:def 10;
      {p}-Ideal = the set of all p * r where r is Element of Polynom-Ring F
      by IDEAL_1:64; then
A26:  q - r in {p}-Ideal by A25;
      f.r = Class(EqRel(Polynom-Ring F,{p}-Ideal),r) by A23,Def8
      .= Class(EqRel(Polynom-Ring F,{p}-Ideal),q) by A26,RING_1:6;
      hence x in rng f by A20,A24,FUNCT_1:3;
    end;
    hence f is onto by A18,TARSKI:2;
  end;
end;

registration
  let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
  cluster KroneckerField(F,p) -> (Polynom-Ring p)-homomorphic
                                 (Polynom-Ring p)-monomorphic
                                 (Polynom-Ring p)-isomorphic;
  coherence
  proof
A1: KroneckerIso p is linear one-to-one;
    hence KroneckerField(F,p) is (Polynom-Ring p)-homomorphic by RING_2:def 4;
    thus
    KroneckerField(F,p) is (Polynom-Ring p)-monomorphic by A1,RING_3:def 3;
    thus
    KroneckerField(F,p) is (Polynom-Ring p)-isomorphic by A1,RING_3:def 4;
  end;
  cluster Polynom-Ring p -> (KroneckerField(F,p))-homomorphic
                            (KroneckerField(F,p))-monomorphic
                            (KroneckerField(F,p))-isomorphic;
  coherence
  proof
    reconsider g = (KroneckerIso p)" as Isomorphism of
                    KroneckerField(F,p),Polynom-Ring p by RING_3:73;
    g is Homomorphism of KroneckerField(F,p),Polynom-Ring p;
    hence Polynom-Ring p is (KroneckerField(F,p))-homomorphic by RING_2:def 4;
    g is monomorphism;
    hence Polynom-Ring p is (KroneckerField(F,p))-monomorphic by RING_3:def 3;
    g is Isomorphism of KroneckerField(F,p),Polynom-Ring p;
    hence Polynom-Ring p is (KroneckerField(F,p))-isomorphic by RING_3:def 4;
  end;
  cluster Polynom-Ring p -> F-homomorphic F-monomorphic;
  coherence;
end;

Lm11:
   for F being polynomial_disjoint Field
   for p being irreducible Element of the carrier of Polynom-Ring F
   ex E being FieldExtension of F st p is_with_roots_in E
   proof
     let F be polynomial_disjoint Field;
     let p be irreducible Element of the carrier of Polynom-Ring F;
A1:  now assume not F,Polynom-Ring p are_disjoint; then
A2:    ([#]F) /\ ([#]Polynom-Ring p) <> {} by FIELD_2:def 1;
       let a be Element of
       (the carrier of F)/\(the carrier of Polynom-Ring p);
A3:    a in the carrier of F & a in the carrier of Polynom-Ring p
       by A2,XBOOLE_0:def 4;
       the carrier of Polynom-Ring p =
       {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8; then
       consider q being Polynomial of F such that
A4:    a = q & deg q < deg p by A3;
       a in the carrier of Polynom-Ring F by A4,POLYNOM3:def 10; then
       a in ([#]F) /\ ([#]Polynom-Ring F) by A3,XBOOLE_0:def 4;
       hence contradiction by FIELD_3:def 3;
     end;
     reconsider KroneckerIsop = (KroneckerIso p)" as
     Isomorphism of KroneckerField(F,p),Polynom-Ring p by RING_3:73;
     set h = KroneckerIsop * (emb p);
     reconsider h as Function of F,Polynom-Ring p by FUNCT_2:13;
     h is linear one-to-one by RINGCAT1:1; then
     reconsider h as Monomorphism of F,Polynom-Ring p;
     reconsider E = embField h as Field by A1,FIELD_2:12;
     emb_iso h is onto by A1,FIELD_2:15; then
     reconsider embisoh = (emb_iso h)" as Function of Polynom-Ring p,E
     by FUNCT_2:25;
A5:  emb_iso h is linear one-to-one onto
     by A1,FIELD_2:13,FIELD_2:14, FIELD_2:15; then
     reconsider P = (Polynom-Ring p) as E-isomorphic Field by RING_3:def 4;
     reconsider embisoh as Isomorphism of P,E by A5,RING_3:73;
     set iso = embisoh * KroneckerIsop, u = KrRoot p;
     reconsider iso as Function of KroneckerField(F,p),E by FUNCT_2:13;
A6:  iso is RingHomomorphism by RINGCAT1:1; then
     reconsider E as KroneckerField(F,p)-homomorphic Field by RING_2:def 4;
     reconsider iso as Homomorphism of KroneckerField(F,p),E by A6;
     u is_a_root_of emb(p,p) by FIELD_1:42; then
A7:  eval((PolyHom iso).(emb(p,p)),iso.u) = 0.E by FIELD_1:33,POLYNOM5:def 7;
     F is Subfield of E by FIELD_2:17; then
     reconsider E as FieldExtension of F by Th4;
     take E;
     reconsider a = iso.u as Element of E;
     (PolyHom iso).(emb(p,p)) = p
     proof
       set g = (PolyHom iso).(emb(p,p));
A8:    KroneckerField(F,p) = (Polynom-Ring F)/({p}-Ideal) by FIELD_1:def 3;
A9:    for a being Element of F holds h.a = a|F
       proof
         let a be Element of F;
         dom(emb p) = the carrier of F by FUNCT_2:def 1; then
A10:     h.a = KroneckerIsop.((emb p).a) by FUNCT_1:13
         .= KroneckerIsop.Class(EqRel(Polynom-Ring F,{p}-Ideal),a|F)
         by FIELD_1:39;
A11:     the carrier of Polynom-Ring p =
         {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
         deg(a|F) <= 0 & deg p > 0 by RATFUNC1:def 2,RING_4:def 4; then
         a|F in the carrier of Polynom-Ring p by A11; then
         reconsider b1 = a|F as Element of Polynom-Ring p;
A12:     dom(KroneckerIso p) = the carrier of Polynom-Ring p by FUNCT_2:def 1;
         (KroneckerIso p).b1
         = Class(EqRel(Polynom-Ring F,{p}-Ideal),b1) by Def8;
         hence thesis by A12,A10,FUNCT_1:32;
       end;
A13:   for a being Element of F holds iso.((emb p).a) = a
       proof
         let a be Element of F;
         rng KroneckerIso p = the carrier of KroneckerField(F,p)
         by FUNCT_2:def 3; then
A14:     dom KroneckerIsop = the carrier of KroneckerField(F,p) by FUNCT_1:33;
         reconsider b = a|F as Element of the carrier of Polynom-Ring F
         by POLYNOM3:def 10;
A15:     the carrier of Polynom-Ring p =
         {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
         deg(a|F) <= 0 & deg p > 0 by RATFUNC1:def 2,RING_4:def 4; then
         a|F in the carrier of Polynom-Ring p by A15; then
         reconsider b1 = a|F as Element of Polynom-Ring p;
         reconsider v = Class(EqRel(Polynom-Ring F,{p}-Ideal),b)
         as Element of KroneckerField(F,p) by A8,RING_1:12;
A16:     (KroneckerIso p).b1
         = Class(EqRel(Polynom-Ring F,{p}-Ideal),b1) by Def8;
A17:     dom(KroneckerIso p) = the carrier of Polynom-Ring p by FUNCT_2:def 1;
         the carrier of (embField h) = carr h by FIELD_2:def 7
         .= (([#]Polynom-Ring p) \ (rng h)) \/ ([#]F)
         by FIELD_2:def 2; then
         reconsider a1 = a as Element of embField h by XBOOLE_0:def 3;
         a in F; then
A18:     (emb_iso h).a1 = h.a by FIELD_2:def 8 .= a|F by A9;
A19:     dom(emb_iso h) = the carrier of embField h by FUNCT_2:def 1;
         thus iso.((emb p).a) = iso.v by FIELD_1:39
         .= embisoh.(KroneckerIsop.v) by A14,FUNCT_1:13
         .= embisoh.b by A16,A17,FUNCT_1:32
         .= a by A18,A19,FUNCT_1:32;
       end;
       now let x be object;
         assume x in NAT; then
         reconsider i = x as Element of NAT;
         g.i = iso.(emb(p,p).i) by FIELD_1:def 2
         .= iso.(Class(EqRel(Polynom-Ring F,{p}-Ideal),(p.i)|F)) by FIELD_1:40
         .= iso.((emb p).(p.i)) by FIELD_1:39;
         hence g.x = p.x by A13;
       end;
       hence thesis;
     end; then
     a is_a_root_of p,E by A7,Th15;
     hence thesis;
   end;

theorem :: Kronecker
   for F being polynomial_disjoint Field
   for f being non constant Element of the carrier of Polynom-Ring F
   ex E being FieldExtension of F st f is_with_roots_in E
   proof
     let F be polynomial_disjoint Field;
     let f be non constant Element of the carrier of Polynom-Ring F;
     consider p being Element of the carrier of Polynom-Ring F such that
A1:  p is_a_irreducible_factor_of f by FIELD_1:3;
     reconsider p as irreducible Element of the carrier of Polynom-Ring F
     by A1,FIELD_1:def 1;
     consider q being Element of the carrier of Polynom-Ring F such that
A2:  p * q = f by A1,FIELD_1:def 1,GCD_1:def 1;
     consider E being FieldExtension of F such that
A3:  p is_with_roots_in E by Lm11;
     take E;
     consider a being Element of E such that
A4:  a is_a_root_of p,E by A3;
     reconsider p1 = p, q1 = q as Polynomial of F;
A5:  F is Subring of E by Def1;
     Ext_eval(f,a) = Ext_eval(p1*'q1,a) by A2,POLYNOM3:def 10
     .= Ext_eval(p1,a) * Ext_eval(q1,a) by A5,ALGNUM_1:20
     .= 0.E by A4; then
     a is_a_root_of f,E;
     hence thesis;
   end;

subset_name: curated