The Mizar article:

The Algebra of Polynomials

by
Ewa Gradzka

Received February 24, 2001

Copyright (c) 2001 Association of Mizar Users

MML identifier: POLYALG1
[ MML identifier index ]


environ

 vocabulary VECTSP_1, FUNCSDOM, RLVECT_1, BINOP_1, FUNCT_1, FUNCOP_1, VECTSP_2,
      LATTICES, RELAT_1, NORMSP_1, ARYTM_3, POLYNOM3, ARYTM_1, GROUP_1,
      ALGSTR_1, ALGSTR_2, FINSEQ_1, RFINSEQ, MATRIX_2, FINSEQ_4, BOOLE,
      UNIALG_2, RLSUB_1, SETFAM_1, POLYNOM1, ALGSEQ_1, POLYALG1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      STRUCT_0, PRE_TOPC, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_4,
      FINSOP_1, RFINSEQ, BINOP_1, BINARITH, GROUP_1, RLVECT_1, VECTSP_1,
      VECTSP_2, NORMSP_1, POLYNOM1, ALGSTR_1, ALGSEQ_1, POLYNOM3, POLYNOM5,
      VECTSP_4;
 constructors REAL_1, MONOID_0, DOMAIN_1, ALGSTR_2, FINSOP_1, RFINSEQ,
      BINARITH, POLYNOM1, GOBOARD1, POLYNOM3, POLYNOM5, VECTSP_4, MEMBERED;
 clusters SUBSET_1, FUNCT_1, STRUCT_0, RELSET_1, VECTSP_1, VECTSP_2, ALGSTR_2,
      FINSEQ_5, ARYTM_3, BINOM, POLYNOM3, POLYNOM5, MEMBERED;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4;
 theorems AXIOMS, TARSKI, NAT_1, RLVECT_1, VECTSP_1, BINARITH, FUNCT_1,
      FUNCT_2, FUNCOP_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, FINSEQ_5, RFINSEQ,
      BINOP_1, GOBOARD1, GOBOARD9, POLYNOM1, POLYNOM3, STRUCT_0, ZFMISC_1,
      POLYNOM5, BINOM, RELAT_1, VECTSP_4, SETFAM_1, ALGSTR_1, XBOOLE_0,
      XBOOLE_1, XCMPLX_1;
 schemes FUNCT_2, SETFAM_1;

begin :: Preliminaries

definition let F be 1-sorted;
 struct ( doubleLoopStr,VectSpStr over F ) AlgebraStr over F (#
         carrier -> set,
         add, mult -> BinOp of the carrier,
         Zero, unity -> Element of the carrier,
         lmult -> Function of [:the carrier of F,the carrier:],
                                      the carrier #);
end;

definition let L be non empty doubleLoopStr;
cluster strict non empty AlgebraStr over L;
existence
 proof
  consider a being BinOp of {0};
  reconsider z=0 as Element of {0} by TARSKI:def 1;
    0 in {0} by TARSKI:def 1;
  then reconsider lm = [:the carrier of L,{0}:]-->0 as
  Function of [:the carrier of L,{0}:],{0} by FUNCOP_1:57;
  take A = AlgebraStr(#{0}, a, a, z, z, lm #);
  thus A is strict non empty by STRUCT_0:def 1;
 end;
end;

definition
let L be non empty doubleLoopStr, A be non empty AlgebraStr over L;
attr A is mix-associative means
   for a being Element of L, x,y being Element of A holds
 a*(x*y) = (a*x)*y;
end;

definition let L be non empty doubleLoopStr;
  cluster well-unital distributive VectSp-like mix-associative
    (non empty AlgebraStr over L);
existence
proof
consider a being BinOp of {0};
reconsider z=0 as Element of {0} by TARSKI:def 1;
  0 in {0} by TARSKI:def 1;
then reconsider lm = [:the carrier of L,{0}:]-->0 as
Function of [:the carrier of L,{0}:],{0} by FUNCOP_1:57;
reconsider A = AlgebraStr(#{0}, a, a, z, z, lm #)
  as non empty AlgebraStr over L by STRUCT_0:def 1;
take A;
A1: for x,y being Element of A holds x = y
 proof let x,y be Element of A;
     x = 0 & y = 0 by TARSKI:def 1;
  hence thesis;
 end;
thus A is well-unital
proof
  let x be Element of A;
  thus x*(1_ A) = x & (1_ A)*x = x by A1;
end;
thus A is distributive
proof
  let x,y,z be Element of A;
  thus x*(y+z) = x*y+x*z & (y+z)*x = y*x+z*x by A1;
end;
thus A is VectSp-like
proof
  let x,y be Element of L;
  let v,w being Element of A;
  thus x*(v+w) = x*v+x*w &
      (x+y)*v = x*v+y*v &
      (x*y)*v = x*(y*v) &
      (1_ L)*v = v by A1;
end;
thus A is mix-associative
proof
  let a be Element of L, x,y be Element of A;
  thus a*(x*y) = (a*x)*y by A1;
end;
end;
end;

definition let L be non empty doubleLoopStr;
  mode Algebra of L is well-unital distributive VectSp-like mix-associative
    (non empty AlgebraStr over L);
end;

theorem Th1:
for X,Y being set
for f being Function of [:X,Y:],X holds dom f = [:X,Y:]
proof
 let X,Y be set;
 let f be Function of [:X,Y:],X;
   X is empty implies [:X,Y:] is empty by ZFMISC_1:113;
 hence dom f = [:X,Y:] by FUNCT_2:def 1;
end;

theorem Th2:
for X,Y being set
for f being Function of [:X,Y:],Y holds dom f = [:X,Y:]
proof
 let X,Y be set;
 let f be Function of [:X,Y:],Y;
   Y is empty implies [:X,Y:] is empty by ZFMISC_1:113;
 hence dom f = [:X,Y:] by FUNCT_2:def 1;
end;

begin :: The Algebra of Formal Power Series

definition
 let L be non empty doubleLoopStr;
 func Formal-Series L -> strict non empty AlgebraStr over L means :Def2:
    (for x be set holds x in the carrier of it iff x is sequence of L) &
    (for x,y be Element of it, p,q be sequence of L st
      x = p & y = q holds x+y = p+q) &
    (for x,y be Element of it, p,q be sequence of L st
      x = p & y = q holds x*y = p*'q) &
    (for a be Element of L, x be Element of it,
    p be sequence of L st x = p holds a*x = a*p) &
    0.it = 0_.(L) &
    1_(it) = 1_.(L);
  existence
   proof
    A1: 0_.(L) in {x where x is sequence of L : not contradiction};
    then reconsider Ca = {x where x is sequence of L : not contradiction}
                                                            as non empty set;
    defpred P[set,set,set] means
     ex p,q be sequence of L st p=$1 & q=$2 & $3=p+q;
    A2: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
    proof
     let x,y be Element of Ca;
       x in Ca;
     then consider p be sequence of L such that
      A3: x=p;
       y in Ca;
     then consider q be sequence of L such that
      A4: y=q;
       p+q in Ca;
     then reconsider u=p+q as Element of Ca;
     take u,p,q;
     thus thesis by A3,A4;
    end;
    consider Ad be Function of [:Ca,Ca:],Ca such that
     A5: for x,y be Element of Ca holds P[x,y,Ad.[x,y]] from FuncEx2D(A2);
    defpred P[set,set,set] means
     ex p,q be sequence of L st p=$1 & q=$2 & $3=p*'q;
    A6: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
    proof
     let x,y be Element of Ca;
       x in Ca;
     then consider p be sequence of L such that
      A7: x=p;
       y in Ca;
     then consider q be sequence of L such that
      A8: y=q;
       p*'q in Ca;
     then reconsider u=p*'q as Element of Ca;
     take u,p,q;
     thus thesis by A7,A8;
    end;
    consider Mu be Function of [:Ca,Ca:],Ca such that
     A9: for x,y be Element of Ca holds P[x,y,Mu.[x,y]] from FuncEx2D(A6);
      1_.(L) in {x where x is sequence of L : not contradiction};
    then reconsider Un = 1_.(L) as Element of Ca;
    reconsider Ze = 0_.(L) as Element of Ca by A1;
    defpred P[Element of L,set,set] means
     ex p be sequence of L st p=$2 & $3=$1*p;
    A10: for a being Element of L,x be Element of Ca
     ex u be Element of Ca st P[a,x,u]
    proof
     let a being Element of L,x be Element of Ca;
       x in Ca;
     then consider q be sequence of L such that A11: x = q;
       a*q in Ca;
     then reconsider u = a*q as Element of Ca;
      take u,q;
      thus thesis by A11;
    end;
    consider lm being Function of [:the carrier of L,Ca:],Ca such that
     A12: for a being Element of L,x be Element of Ca holds
      P[a,x,lm.[a,x]] from FuncEx2D(A10);
    reconsider P = AlgebraStr(# Ca, Ad, Mu, Ze, Un, lm #)
    as strict non empty AlgebraStr over L by STRUCT_0:def 1;
    take P;
    thus for x be set holds x in the carrier of P iff x is sequence of L
    proof
     let x be set;
     thus x in the carrier of P implies x is sequence of L
     proof
      assume x in the carrier of P;
      then consider p be sequence of L such that
       A13: x=p;
      thus x is sequence of L by A13;
     end;
     thus thesis;
    end;
    thus for x,y be Element of P, p,q be sequence of L st
     x = p & y = q holds x+y = p+q
    proof
     let x,y be Element of P;
     let p,q be sequence of L;
     assume that
      A14: x = p and
      A15: y = q;
     consider p1,q1 be sequence of L such that
      A16: p1 = x and
      A17: q1 = y and
      A18: Ad.[x,y] = p1+q1 by A5;
     thus x+y = p+q by A14,A15,A16,A17,A18,RLVECT_1:def 3;
    end;
    thus for x,y be Element of P, p,q be sequence of L st
     x = p & y = q holds x*y = p*'q
    proof
     let x,y be Element of P;
     let p,q be sequence of L;
     assume that
      A19: x = p and
      A20: y = q;
     consider p1,q1 be sequence of L such that
      A21: p1 = x and
      A22: q1 = y and
      A23: Mu.[x,y] = p1*'q1 by A9;
     thus x*y = Mu.(x,y) by VECTSP_1:def 10
             .= p*'q by A19,A20,A21,A22,A23,BINOP_1:def 1;
    end;

    thus for a be Element of L, x be Element of P,
    p be sequence of L st x = p holds a*x = a*p
     proof
      let a be Element of L, x be Element of P,
    p be sequence of L such that A24:x = p;
    consider p1 being sequence of L such that A25: x = p1 and
      A26: lm.[a,x]=a*p1 by A12;
    thus a*x = (the lmult of P).(a,x) by VECTSP_1:def 24
            .= a*p by A24,A25,A26,BINOP_1:def 1;
    end;
    thus 0.P = 0_.(L) by RLVECT_1:def 2;
    thus 1_(P) = 1_.(L) by VECTSP_1:def 9;
   end;

   uniqueness
   proof
    let P1,P2 be strict non empty AlgebraStr over L such that
     A27: for x be set holds x in the carrier of P1 iff x is sequence of L and
     A28: for x,y be Element of P1, p,q be sequence of L st
      x = p & y = q holds x+y = p+q and
     A29: for x,y be Element of P1, p,q be sequence of L st
      x = p & y = q holds x*y = p*'q and
     A30: for a be Element of L, x be Element of P1,
    p be sequence of L st x = p holds a*x = a*p and
     A31: 0.P1 = 0_.(L) and
     A32: 1_(P1) = 1_.(L) and
     A33: for x be set holds x in the carrier of P2 iff x is sequence of L and
     A34: for x,y be Element of P2, p,q be sequence of L st
      x = p & y = q holds x+y = p+q and
     A35: for x,y be Element of P2, p,q be sequence of L st
      x = p & y = q holds x*y = p*'q and
     A36: for a be Element of L, x be Element of P2,
    p be sequence of L st x = p holds a*x = a*p and
     A37: 0.P2 = 0_.(L) and
     A38: 1_(P2) = 1_.(L);
    A39: now let x be set;
       x in the carrier of P1 iff x is sequence of L by A27;
     hence x in the carrier of P1 iff x in the carrier of P2 by A33;
    end;
    then A40: the carrier of P1 = the carrier of P2 by TARSKI:2;
      now let x be Element of P1,
            y be Element of P2;
     reconsider x1=x as Element of P2 by A39;
     reconsider y1=y as Element of P1 by A39;
     reconsider p=x as sequence of L by A27;
     reconsider q=y as sequence of L by A33;
     thus (the add of P1).(x,y) = x+y1 by RLVECT_1:5
        .= p+q by A28
        .= x1+y by A34
        .= (the add of P2).(x,y) by RLVECT_1:5;
    end;
    then A41: the add of P1 = the add of P2 by A40,BINOP_1:2;
    A42: now let x be Element of P1,
            y be Element of P2;
     reconsider x1=x as Element of P2 by A39;
     reconsider y1=y as Element of P1 by A39;
     reconsider p=x as sequence of L by A27;
     reconsider q=y as sequence of L by A33;
     thus (the mult of P1).(x,y) = x*y1 by VECTSP_1:def 10
        .= p*'q by A29
        .= x1*y by A35
        .= (the mult of P2).(x,y) by VECTSP_1:def 10;
    end;
      now let a be Element of L,
            x be Element of P1;
     reconsider a1=a as Element of L;
     reconsider x1=x as Element of P2 by A39;
     reconsider p=x as sequence of L by A27;
     thus (the lmult of P1).(a,x) = a*x by VECTSP_1:def 24
        .= a1*p by A30
        .= a1*x1 by A36
        .= (the lmult of P2).(a,x) by VECTSP_1:def 24;
    end;
    then A43: the lmult of P1=the lmult of P2 by A40,BINOP_1:2;
    A44: the unity of P1 = 1_.(L) by A32,VECTSP_1:def 9
       .= the unity of P2 by A38,VECTSP_1:def 9;
      the Zero of P1 = 0_.(L) by A31,RLVECT_1:def 2
       .= the Zero of P2 by A37,RLVECT_1:def 2;
    hence P1 = P2 by A40,A41,A42,A43,A44,BINOP_1:2;
   end;
  end;

  definition
   let L be Abelian (non empty doubleLoopStr);
   cluster Formal-Series L -> Abelian;
   coherence
   proof
    let p,q be Element of Formal-Series L;
    reconsider p1=p, q1=q as sequence of L by Def2;
    thus p + q = p1 + q1 by Def2
       .= q + p by Def2;
   end;
  end;

  definition
   let L be add-associative (non empty doubleLoopStr);
   cluster Formal-Series L -> add-associative;
   coherence
   proof
    let p,q,r be Element of Formal-Series L;
    reconsider p1=p, q1=q, r1=r as sequence of L by Def2;
    A1: q + r = q1 + r1 by Def2;
      p + q = p1 + q1 by Def2;
    hence (p + q) + r = (p1 + q1) + r1 by Def2
       .= p1 + (q1 + r1) by POLYNOM3:26
       .= p + (q + r) by A1,Def2;
   end;
  end;

  definition
   let L be right_zeroed (non empty doubleLoopStr);
   cluster Formal-Series L -> right_zeroed;
   coherence
   proof
    let p be Element of Formal-Series L;
    reconsider p1=p as sequence of L by Def2;
      0.(Formal-Series L) = 0_.(L) by Def2;
    hence p + 0.(Formal-Series L) = p1 + 0_.(L) by Def2
       .= p by POLYNOM3:29;
   end;
  end;

  definition
   let L be add-associative right_zeroed right_complementable
    (non empty doubleLoopStr);
   cluster Formal-Series L -> right_complementable;
   coherence
   proof
    let p be Element of Formal-Series L;
    reconsider p1=p as sequence of L by Def2;
    reconsider q = -p1 as Element of Formal-Series L by Def2;
    take q;
    thus p + q = p1 + -p1 by Def2
       .= p1 - p1 by POLYNOM3:def 8
       .= 0_.(L) by POLYNOM3:30
       .= 0.(Formal-Series L) by Def2;
   end;
  end;

  definition
   let L be Abelian add-associative right_zeroed commutative
                     (non empty doubleLoopStr);
   cluster Formal-Series L -> commutative;
   coherence
   proof
    let p,q be Element of Formal-Series L;
    reconsider p1=p, q1=q as sequence of L by Def2;
    thus p * q = p1 *' q1 by Def2
       .= q * p by Def2;
   end;
  end;

  definition
   let L be Abelian add-associative right_zeroed right_complementable
   unital associative distributive (non empty doubleLoopStr);
   cluster Formal-Series L -> associative;
   coherence
   proof
    let p,q,r be Element of Formal-Series L;
    reconsider p1=p, q1=q, r1=r as sequence of L by Def2;
    A1: q * r = q1 *' r1 by Def2;
      p * q = p1 *' q1 by Def2;
    hence (p * q) * r = (p1 *' q1) *' r1 by Def2
       .= p1 *' (q1 *' r1) by POLYNOM3:34
       .= p * (q * r) by A1,Def2;
   end;
  end;

definition
   let L be add-associative right_zeroed right_complementable right_unital
        right-distributive (non empty doubleLoopStr);
   cluster Formal-Series L -> right_unital;
   coherence
   proof
    let p be Element of Formal-Series L;
    reconsider p1=p as sequence of L by Def2;
      1_(Formal-Series L) = 1_.(L) by Def2;
    hence p * 1_(Formal-Series L) = p1 *' 1_.(L) by Def2
       .= p by POLYNOM3:36;
   end;
end;

definition
  cluster add-associative associative right_zeroed left_zeroed
    right_unital left_unital
    right_complementable distributive (non empty doubleLoopStr);
  existence
  proof
    take F_Real; thus thesis;
  end;
end;

  theorem Th3:
   for D be non empty set
   for f being non empty FinSequence of D holds
    f/^1 = Del(f,1)
    proof
     let D be non empty set;
     let f be non empty FinSequence of D;
     consider i be Nat such that A1: i+1 = len f by FINSEQ_5:7;
A2:  1 <= len f by A1,NAT_1:29;
       (len (f/^1) = len Del(f,1)) & for k be Nat st 1 <=k & k <= len (f/^1)
     holds (f/^1).k=Del(f,1).k
      proof
A3:    1 in dom f by FINSEQ_5:6;
A4:    len (f/^1) = (i+1)-1 by A1,A2,RFINSEQ:def 2
                 .= i by XCMPLX_1:26;
       hence len (f/^1) = len Del(f,1) by A1,A3,GOBOARD1:6;
       let k be Nat such that
A5:    1 <=k & k <= len (f/^1);
A6:    1 in dom f & 1<=k & k<=i by A4,A5,FINSEQ_5:6;
     k in dom (f/^1) by A5,FINSEQ_3:27;
       hence (f/^1).k= f.(k+1) by A2,RFINSEQ:def 2
                   .= Del(f,1).k by A1,A6,GOBOARD1:9;
      end;
     hence thesis by FINSEQ_1:18;
    end;

  theorem Th4:
   for D be non empty set
   for f being non empty FinSequence of D holds
   f = <*f.1*>^Del(f,1)
    proof
     let D be non empty set;
     let f be non empty FinSequence of D;
     A1: 1 in dom f by FINSEQ_5:6;
     thus f = <*f/.1*>^(f/^1) by FINSEQ_5:32
           .= <*f.1*>^(f/^1) by A1,FINSEQ_4:def 4
           .= <*f.1*>^Del(f,1) by Th3;
    end;

  theorem Th5:
   for L be add-associative right_zeroed left_unital right_complementable
    left-distributive (non empty doubleLoopStr)
   for p be sequence of L holds
   (1_.(L))*'p = p
   proof
    let L be add-associative right_zeroed left_unital right_complementable
     left-distributive (non empty doubleLoopStr);
    let p be sequence of L;
      now let i be Nat;
     consider r be FinSequence of the carrier of L such that
      A1: len r = i+1 and
      A2: ((1_.(L))*'p).i = Sum r and
      A3: for k be Nat st k in dom r holds r.k = (1_.(L)).(k-'1)*p.(i+1-'k)
      by POLYNOM3:def 11;
        i >=0 by NAT_1:18;
      then i+1>0 by NAT_1:38;
      then A4: r <> {} by A1,FINSEQ_1:25;
     then A5: 1 in dom r by FINSEQ_5:6;
       r = <*r.1*>^Del(r,1) by A4,Th4
      .= <*r/.1*>^Del(r,1) by A5,FINSEQ_4:def 4;
     then A6: Sum r = Sum <*r/.1*> + Sum Del(r,1) by RLVECT_1:58
        .= r/.1 + Sum Del(r,1)by RLVECT_1:61;
       now let k be Nat;
       assume A7: k in dom Del(r,1);
          len Del(r,1) = i by A1,A5,GOBOARD1:6;
       then A8: 0+1 <= k & k <= i by A7,FINSEQ_3:27;
      then A9:  k+1 <= i+ 1 by AXIOMS:24;
          k+1 >= 1 by NAT_1:29;
      then A10: k+1 in dom r by A1,A9,FINSEQ_3:27;
      A11: k<>0 by A7,FINSEQ_3:27;
      thus Del(r,1).k = r.(k+1) by A1,A5,A8,GOBOARD1:9
         .= (1_.(L)).(k+1-'1)*p.(i+1-'(k+1)) by A3,A10
         .= (1_.(L)).(k)*p.(i+1-'(k+1)) by BINARITH:39
         .= 0.(L)*p.(i+1-'(k+1)) by A11,POLYNOM3:31
         .= 0.(L) by VECTSP_1:39;
     end;
     then A12: Sum Del(r,1) = 0.(L) by POLYNOM3:1;
       r/.1 = r.1 by A5,FINSEQ_4:def 4
        .= (1_.(L)).(1-'1)*p.(i+1-'1) by A3,A5
        .= (1_.(L)).(1-'1)*p.i by BINARITH:39
        .= (1_.(L)).(0)*p.i by GOBOARD9:1
        .= 1_(L)*p.i by POLYNOM3:31
        .= p.i by VECTSP_1:def 19;
     hence ((1_.(L))*'p).i = p.i by A2,A6,A12,RLVECT_1:10;
    end;
    hence (1_.(L))*'p = p by FUNCT_2:113;
   end;

definition
   let L be add-associative right_zeroed right_complementable left_unital
    left-distributive (non empty doubleLoopStr);
   cluster Formal-Series L -> left_unital;
   coherence
   proof
    let p be Element of Formal-Series L;
    reconsider p1=p as sequence of L by Def2;
      1_(Formal-Series L) = 1_.(L) by Def2;
    hence 1_(Formal-Series L)*p = (1_.(L)) *' p1 by Def2
       .= p by Th5;
   end;
end;

definition
   let L be Abelian add-associative right_zeroed right_complementable
           distributive (non empty doubleLoopStr);
   cluster Formal-Series L -> right-distributive;
   coherence
   proof
    let p,q,r be Element of Formal-Series L;
    reconsider p1=p, q1=q, r1=r as sequence of L by Def2;
    A1: p*q = p1*'q1 & p*r = p1*'r1 by Def2;
      q+r = q1+r1 by Def2;
    hence p*(q+r) = p1*'(q1+r1) by Def2
       .= p1*'q1+p1*'r1 by POLYNOM3:32
       .= p*q+p*r by A1,Def2;
   end;

   cluster Formal-Series L -> left-distributive;
   coherence
   proof
    let p,q,r be Element of Formal-Series L;
    reconsider p1=p, q1=q, r1=r as sequence of L by Def2;
    A2: q*p = q1*'p1 & r*p = r1*'p1 by Def2;
      q+r = q1+r1 by Def2;
    hence (q+r)*p = (q1+r1)*'p1 by Def2
       .= q1*'p1+r1*'p1 by POLYNOM3:33
       .= q*p+r*p by A2,Def2;
   end;
end;

theorem Th6:
   for L be Abelian add-associative right_zeroed
   right_complementable distributive (non empty doubleLoopStr)
   for a being Element of L, p,q being sequence of L holds
   a*(p+q)=a*p + a*q
   proof
    let L be Abelian add-associative right_zeroed
     right_complementable distributive (non empty doubleLoopStr);
    let a be Element of L, p,q be sequence of L;
      for i be Element of NAT holds (a*(p+q)).i = (a*p + a*q).i
     proof
      let i be Element of NAT;
         a*((p+q).i) = a*(p.i + q.i) by POLYNOM3:def 6
                  .= a*(p.i) + a*(q.i) by VECTSP_1:def 18
                  .= (a*p).i + a*(q.i) by POLYNOM5:def 3
                  .= (a*p).i + (a*q).i by POLYNOM5:def 3
                  .= (a*p + a*q).i by POLYNOM3:def 6;
      hence (a*(p+q)).i = (a*p + a*q).i by POLYNOM5:def 3;
     end;
    hence thesis by FUNCT_2:113;
   end;

theorem Th7:
   for L be Abelian add-associative right_zeroed
   right_complementable distributive (non empty doubleLoopStr)
   for a,b being Element of L, p being sequence of L holds
   (a+b)*p = a*p + b*p
   proof
    let L be Abelian add-associative right_zeroed
     right_complementable distributive (non empty doubleLoopStr);
    let a,b be Element of L, p be sequence of L;
      for i be Element of NAT holds ((a+b)*p).i = (a*p + b*p).i
     proof
      let i be Element of NAT;
      thus ((a+b)*p).i = (a+b)*p.i by POLYNOM5:def 3
        .= a*p.i + b*p.i by VECTSP_1:def 18
        .= (a*p).i + b*p.i by POLYNOM5:def 3
        .= (a*p).i + (b*p).i by POLYNOM5:def 3
        .= (a*p + b*p).i by POLYNOM3:def 6;
     end;
    hence thesis by FUNCT_2:113;
   end;

theorem Th8:
   for L be associative (non empty doubleLoopStr)
   for a,b being Element of L, p being sequence of L holds
   (a*b)*p = a*(b*p)
    proof
     let L be associative (non empty doubleLoopStr);
     let a,b being Element of L, p being sequence of L;
       for i be Element of NAT holds ((a*b)*p).i = (a*(b*p)).i
      proof
       let i be Element of NAT;
       thus ((a*b)*p).i = (a*b)*p.i by POLYNOM5:def 3
         .= a*(b*(p.i)) by VECTSP_1:def 16
         .= a*(b*p).i by POLYNOM5:def 3
         .= (a*(b*p)).i by POLYNOM5:def 3;
      end;
     hence thesis by FUNCT_2:113;
    end;

theorem Th9:
   for L be associative left_unital (non empty doubleLoopStr)
   for p being sequence of L holds
   (the unity of L)*p = p
    proof
     let L be associative left_unital (non empty doubleLoopStr);
     let p be sequence of L;
       for i being Element of NAT holds ((the unity of L)*p).i = p.i
      proof
       let i be Element of NAT;
       thus ((the unity of L)*p).i = (the unity of L)*p.i by POLYNOM5:def 3
        .= (1_ L)*p.i by VECTSP_1:def 9
        .= p.i by VECTSP_1:def 19;
      end;
     hence thesis by FUNCT_2:113;
    end;

definition
   let L be Abelian add-associative associative right_zeroed
   right_complementable left_unital distributive (non empty doubleLoopStr);
   cluster Formal-Series L -> VectSp-like;
   coherence
   proof
    let x,y be Element of L;
    reconsider x'=x, y'=y as Element of L;
    let v,w being Element of Formal-Series L;
    reconsider p=v, q=w as sequence of L by Def2;
A1: x*v = x*p by Def2;
A2: x*w = x*q by Def2;
A3: y*v = y*p by Def2;
    reconsider k=v+w as Element of Formal-Series L;
    reconsider r=k as sequence of L by Def2;
  x*k = x*r by Def2;
hence x*(v+w) = x*(p+q) by Def2
       .= x'*p + x'*q by Th6
       .= x*v + x*w by A1,A2,Def2;
thus (x+y)*v = (x'+y')*p by Def2
       .= x'*p + y'*p by Th7
       .= x*v + y*v by A1,A3,Def2;
thus (x*y)*v = (x'*y')*p by Def2
       .= x'*(y'*p) by Th8
       .= x*(y*v) by A3,Def2;
       reconsider u = the unity of L as Element of L;
thus (1_ L)*v = (the unity of L)*v by VECTSP_1:def 9
       .= u*p by Def2
       .= v by Th9;
   end;
end;

theorem Th10:
  for L be Abelian left_zeroed add-associative associative right_zeroed
   right_complementable distributive (non empty doubleLoopStr)
   for a being Element of L, p,q being sequence of L holds
   a*(p*'q)=(a*p)*'q
    proof
     let L be Abelian left_zeroed add-associative associative right_zeroed
     right_complementable distributive (non empty doubleLoopStr);
     let a being Element of L, p,q being sequence of L;
       for x being Element of NAT holds (a*(p*'q)).x = ((a*p)*'q).x
      proof
       let i be Element of NAT;
       consider f1 be FinSequence of the carrier of L such that
A1:    len f1 = i+1 and
A2:    (p*'q).i = Sum f1 and
A3:    for k be Nat st k in dom f1 holds f1.k = p.(k-'1) * q.(i+1-'k) by
POLYNOM3:def 11;
       consider f2 be FinSequence of the carrier of L such that
A4:    len f2 = i+1 and
A5:    ((a*p)*'q).i = Sum f2 and
A6:    for k be Nat st k in dom f2 holds f2.k = (a*p).(k-'1) * q.(i+1-'k) by
POLYNOM3:def 11;
A7:    dom (a*f1) = dom f1 by POLYNOM1:def 2
         .= dom f2 by A1,A4,FINSEQ_3:31;
A8:    for k be Nat st k in dom f2 holds f2.k = (a*f1).k
        proof
         let k be Nat such that
A9:      k in dom f2;
A10:      k in dom f1 by A1,A4,A9,FINSEQ_3:31;
then A11:    p.(k-'1) * q.(i+1-'k) = f1.k by A3
          .= f1/.k by A10,FINSEQ_4:def 4;
         thus f2.k = (a*p).(k-'1) * q.(i+1-'k) by A6,A9
         .= a*p.(k-'1) * q.(i+1-'k) by POLYNOM5:def 3
         .= a*(f1/.k) by A11,VECTSP_1:def 16
         .= (a*f1)/.k by A10,POLYNOM1:def 2
         .= (a*f1).k by A7,A9,FINSEQ_4:def 4;
        end;
       thus (a*(p*'q)).i = a*(Sum f1) by A2,POLYNOM5:def 3
         .= Sum (a* f1) by BINOM:4
         .= ((a*p)*'q).i by A5,A7,A8,FINSEQ_1:17;
      end;
     hence thesis by FUNCT_2:113;
    end;

definition
   let L be Abelian left_zeroed add-associative associative right_zeroed
   right_complementable distributive (non empty doubleLoopStr);
   cluster Formal-Series L -> mix-associative;
   coherence
   proof
    let a be Element of L, x,y be Element of Formal-Series L;
    reconsider x1=x, y1=y as Element of Formal-Series L;
    reconsider p=x1, q=y1 as sequence of L by Def2;
A1:    a*x = a*p by Def2;
       x*y = p*'q by Def2;
    hence a*(x*y) = a*(p*'q) by Def2
         .=(a*p)*'q by Th10
         .= (a*x)*y by A1,Def2;
    end;
end;

definition
  let L be left_zeroed right_zeroed add-associative left_unital right_unital
   right_complementable distributive (non empty doubleLoopStr);
  cluster Formal-Series L -> well-unital;
  coherence;
end;

Lm1:
  now let L be 1-sorted, A be AlgebraStr over L;
      dom the add of A = [:the carrier of A,the carrier of A:] by Th2;
    hence
      the add of A = (the add of A)|[:the carrier of A,the carrier of A:] by
RELAT_1:98;
      dom the mult of A = [:the carrier of A,the carrier of A:] by Th2;
    hence
      the mult of A = (the mult of A)|[:the carrier of A,the carrier of A:]
     by RELAT_1:98;
      dom the lmult of A = [:the carrier of L,the carrier of A:] by Th2;
    hence
      the lmult of A = (the lmult of A)|[:the carrier of L,the carrier of A:]
by RELAT_1:98;
 end;

definition
  let L be 1-sorted;
  let A be AlgebraStr over L;
 mode Subalgebra of A -> AlgebraStr over L means :Def3:
  the carrier of it c= the carrier of A & 1_(it) = 1_(A) & 0.it = 0.A &
  the add of it = (the add of A)|[:the carrier of it,the carrier of it:] &
  the mult of it = (the mult of A)|[:the carrier of it,the carrier of it:] &
  the lmult of it = (the lmult of A)|[:the carrier of L,the carrier of it:];
  existence
   proof take A; thus thesis by Lm1; end;
end;

theorem Th11:
 for L being 1-sorted
 for A being AlgebraStr over L holds A is Subalgebra of A
 proof
  let L be 1-sorted;
  let A be AlgebraStr over L;
  thus the carrier of A c= the carrier of A & 1_(A) = 1_(A) & 0.A = 0.A &
  the add of A = (the add of A)|[:the carrier of A,the carrier of A:] &
  the mult of A = (the mult of A)|[:the carrier of A,the carrier of A:] &
  the lmult of A = (the lmult of A)|[:the carrier of L,the carrier of A:]
   by Lm1;
 end;

theorem
   for L being 1-sorted
 for A,B,C being AlgebraStr over L st A is Subalgebra of B &
  B is Subalgebra of C holds A is Subalgebra of C
  proof
   let L be 1-sorted;
   let A,B,C be AlgebraStr over L such that
A1: A is Subalgebra of B and
A2: B is Subalgebra of C;
A3: the carrier of A c= the carrier of B by A1,Def3;
      the carrier of B c= the carrier of C by A2,Def3;
   hence the carrier of A c= the carrier of C by A3,XBOOLE_1:1;
   thus 1_(A) = 1_(B) by A1,Def3 .= 1_(C) by A2,Def3;
   thus 0.A = 0.B by A1,Def3 .= 0.C by A2,Def3;
A4: [:the carrier of A,the carrier of A:] c=
        [:the carrier of B,the carrier of B:] by A3,ZFMISC_1:119;
   thus the add of A = (the add of B)|[:the carrier of A,the carrier of A:]
      by A1,Def3
     .= ((the add of C)|[:the carrier of B,the carrier of B:])|
                             [:the carrier of A,the carrier of A:] by A2,Def3
     .= (the add of C)|[:the carrier of A,the carrier of A:] by A4,FUNCT_1:82;
   thus the mult of A = (the mult of B)|[:the carrier of A,the carrier of A:]
      by A1,Def3
     .= ((the mult of C)|[:the carrier of B,the carrier of B:])|
                             [:the carrier of A,the carrier of A:] by A2,Def3
   .= (the mult of C)|[:the carrier of A,the carrier of A:] by A4,FUNCT_1:82;
A5: [:the carrier of L,the carrier of A:] c=
          [:the carrier of L,the carrier of B:] by A3,ZFMISC_1:119;
   thus
     the lmult of A = (the lmult of B)|[:the carrier of L,the carrier of A:]
         by A1,Def3
       .= ((the lmult of C)|[:the carrier of L,the carrier of B:])|
            [:the carrier of L,the carrier of A:] by A2,Def3
   .= (the lmult of C)|[:the carrier of L,the carrier of A:] by A5,FUNCT_1:82;
  end;

theorem
   for L being 1-sorted
 for A,B being AlgebraStr over L st A is Subalgebra of B &
  B is Subalgebra of A holds the AlgebraStr of A = the AlgebraStr of B
 proof
  let L be 1-sorted;
  let A,B be AlgebraStr over L such that
A1: A is Subalgebra of B and
A2: B is Subalgebra of A;
A3: the carrier of A c= the carrier of B by A1,Def3;
A4: the carrier of B c= the carrier of A by A2,Def3;
then A5: the carrier of A = the carrier of B by A3,XBOOLE_0:def 10;
A6: dom (the add of B) = [:the carrier of B,the carrier of B:] by Th1;
A7: dom (the mult of B) = [:the carrier of B,the carrier of B:] by Th1;
A8:dom (the lmult of B) = [:the carrier of L,the carrier of B:] by Th2;
     A9: [:the carrier of L,the carrier of B:] c=
              [:the carrier of L,the carrier of A:] by A4,ZFMISC_1:119;
A10: the add of A = (the add of B)|[:the carrier of A,the carrier of A:]
      by A1,Def3
     .= the add of B by A5,A6,RELAT_1:97;
A11: the mult of A = (the mult of B)|[:the carrier of A,the carrier of A:]
      by A1,Def3
     .= the mult of B by A5,A7,RELAT_1:97;
A12: the lmult of A = (the lmult of B)|[:the carrier of L,the carrier of A:]
      by A1,Def3
     .= the lmult of B by A8,A9,RELAT_1:97;
A13: the Zero of A = 0.A by RLVECT_1:def 2
     .= 0.B by A1,Def3
     .= the Zero of B by RLVECT_1:def 2;
      the unity of A = 1_(A) by VECTSP_1:def 9
     .= 1_(B) by A1,Def3
     .= the unity of B by VECTSP_1:def 9;
  hence the AlgebraStr of A = the AlgebraStr of B
         by A3,A4,A10,A11,A12,A13,XBOOLE_0:def 10;
 end;

theorem Th14:
for L being 1-sorted
for A,B being AlgebraStr over L st the AlgebraStr of A = the AlgebraStr of B
 holds A is Subalgebra of B & B is Subalgebra of A
proof
let L be 1-sorted;
let A,B be AlgebraStr over L such that
A1: the AlgebraStr of A = the AlgebraStr of B;
A2: dom (the add of B) = [:the carrier of B,the carrier of B:] by Th1;
A3: dom (the mult of B) = [:the carrier of B,the carrier of B:] by Th1;
A4:dom (the lmult of B) = [:the carrier of L,the carrier of B:] by Th2;
A5: dom (the add of A) = [:the carrier of A,the carrier of A:] by Th1;
A6: dom (the mult of A) = [:the carrier of A,the carrier of A:] by Th1;
A7:dom (the lmult of A) = [:the carrier of L,the carrier of A:] by Th2;
thus A is Subalgebra of B
proof
thus the carrier of A c= the carrier of B by A1;
thus 1_(A) = the unity of A by VECTSP_1:def 9
          .= 1_(B) by A1,VECTSP_1:def 9;
thus 0.A = the Zero of A by RLVECT_1:def 2
        .= 0.B by A1,RLVECT_1:def 2;
thus the add of A = (the add of B)|[:the carrier of A,the carrier of A:]
            by A1,A2,RELAT_1:97;
thus the mult of A = (the mult of B)|[:the carrier of A,the carrier of A:]
           by A1,A3,RELAT_1:97;
thus the lmult of A = (the lmult of B)|[:the carrier of L,the carrier of A:]
           by A1,A4,RELAT_1:97;
end;
thus B is Subalgebra of A
proof
  thus the carrier of B c= the carrier of A by A1;
  thus 1_(B) = the unity of B by VECTSP_1:def 9
         .= 1_(A) by A1,VECTSP_1:def 9;
  thus 0.B = the Zero of B by RLVECT_1:def 2
       .= 0.A by A1,RLVECT_1:def 2;
  thus the add of B = (the add of A)|[:the carrier of B,the carrier of B:]
            by A1,A5,RELAT_1:97;
  thus the mult of B = (the mult of A)|[:the carrier of B,the carrier of B:]
         by A1,A6,RELAT_1:97;
  thus the lmult of B = (the lmult of A)|[:the carrier of L,the carrier of B:]
         by A1,A7,RELAT_1:97;
end;
end;

definition
  let L be non empty 1-sorted;
  cluster non empty strict AlgebraStr over L;
existence
proof
  set A = {0};
  consider a being BinOp of A;
  reconsider z=0 as Element of {0} by TARSKI:def 1;
    0 in {0} by TARSKI:def 1;
  then reconsider lm = [:the carrier of L,{0}:]-->0 as
  Function of [:the carrier of L,{0}:],{0} by FUNCOP_1:57;
  take B = AlgebraStr(#{0}, a, a, z, z, lm #);
  thus B is non empty by STRUCT_0:def 1;
  thus B is strict;
end;
end;

definition
  let L be 1-sorted;
  let B be AlgebraStr over L;
  cluster strict Subalgebra of B;
existence
proof
  reconsider b = AlgebraStr(# the carrier of B, the add of B, the mult of B,
        the Zero of B, the unity of B, the lmult of B #)
        as Subalgebra of B by Th14;
  take b;
  thus thesis;
end;
end;

definition
  let L be non empty 1-sorted;
  let B be non empty AlgebraStr over L;
  cluster strict non empty Subalgebra of B;
existence
proof
reconsider b = AlgebraStr(# the carrier of B, the add of B, the mult of B,
        the Zero of B, the unity of B, the lmult of B #)
        as Subalgebra of B by Th14;
take b;
thus thesis by STRUCT_0:def 1;
end;
end;

definition
  let L be non empty HGrStr;
  let B be non empty AlgebraStr over L;
  let A be Subset of B;
  attr A is opers_closed means :Def4:
    A is lineary-closed &
    (for x,y being Element of B st x in A & y in A holds x*y in A) &
    1_(B) in A &
    0.B in A;
end;

theorem Th15:
for L being non empty HGrStr
for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B holds
for x,y being Element of B,
x',y' being Element of A st x = x' & y = y' holds
x+y = x'+ y'
proof
  let L be non empty HGrStr;
  let B be non empty AlgebraStr over L;
  let A be non empty Subalgebra of B;
  let x,y be Element of B,
      x',y' be Element of A such that
A1: x = x' & y = y';
A2: [x',y'] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
thus x+y = (the add of B).[x',y'] by A1,RLVECT_1:def 3
        .= (the add of B)|[:the carrier of A,the carrier of A:].[x',y']
           by A2,FUNCT_1:72
        .= (the add of A).[x',y'] by Def3
        .= x'+ y' by RLVECT_1:def 3;
end;

theorem Th16:
for L be non empty HGrStr
for B be non empty AlgebraStr over L
for A be non empty Subalgebra of B holds
for x,y being Element of B,
x',y' being Element of A st x = x' & y = y' holds
 x*y = x'* y'
proof
let L be non empty HGrStr;
let B be non empty AlgebraStr over L;
let A be non empty Subalgebra of B;
let x,y be Element of B,
   x',y' be Element of A such that
A1: x = x' & y = y';
A2: [x',y'] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
thus x*y = (the mult of B).(x',y') by A1,VECTSP_1:def 10
        .= (the mult of B).[x',y'] by BINOP_1:def 1
        .= (the mult of B)|[:the carrier of A,the carrier of A:].[x',y']
           by A2,FUNCT_1:72
        .= (the mult of A).[x',y'] by Def3
        .= (the mult of A).(x',y') by BINOP_1:def 1
        .= x'* y' by VECTSP_1:def 10;
end;

theorem Th17:
for L be non empty HGrStr
for B be non empty AlgebraStr over L
for A be non empty Subalgebra of B holds
for a being Element of L
for x being Element of B,
x' being Element of A st x = x' holds
 a * x = a * x'
proof
let L be non empty HGrStr;
let B be non empty AlgebraStr over L;
let A be non empty Subalgebra of B;
let a be Element of L;
let x be Element of B,
    x' be Element of A such that
A1: x = x';
A2:  [a,x'] in [:the carrier of L,the carrier of A:] by ZFMISC_1:106;
thus a * x = (the lmult of B).(a,x') by A1,VECTSP_1:def 24
        .= (the lmult of B).[a,x'] by BINOP_1:def 1
        .= (the lmult of B)|[:the carrier of L,the carrier of A:].[a,x']
           by A2,FUNCT_1:72
        .= (the lmult of A).[a,x'] by Def3
        .= (the lmult of A).(a,x') by BINOP_1:def 1
        .= a * x' by VECTSP_1:def 24;
end;

canceled;

theorem
  for L be non empty HGrStr
for B be non empty AlgebraStr over L
for A be non empty Subalgebra of B ex C being Subset of B st
the carrier of A = C & C is opers_closed
proof
 let L be non empty HGrStr;
 let B be non empty AlgebraStr over L;
 let A be non empty Subalgebra of B;
A1: the carrier of A c= the carrier of B by Def3;
 take C = the carrier of A;
reconsider C as Subset of B by A1;
A2: C is lineary-closed
  proof
   thus for v,u being Element of B st v in C & u in C
       holds v + u in C
    proof
     let v,u be Element of B such that
A3:   v in C & u in C;
     reconsider x = u, y = v as Element of A by A3;
        v + u = y + x by Th15;
     hence v + u in C;
    end;
   thus for a being Element of L,
        v being Element of B
     st v in C holds a * v in C
    proof
     let a be Element of L,
      v be Element of B such that
A4:   v in C;
     reconsider x = v as Element of A by A4;
        a * v = a * x by Th17;
     hence a * v in C;
    end;
  end;
A5: 1_(B) = 1_(A) & 0.B = 0.A by Def3;
   for x,y being Element of B st x in C & y in C holds x*y in C
     proof
      let x,y be Element of B such that
A6:    x in C & y in C;
      reconsider x' = x, y' = y as Element of B;
      reconsider x1 = x', y1 = y' as Element of A by A6;
         x*y = x1 * y1 by Th16;
       hence x*y in C;
     end;
 hence thesis by A2,A5,Def4;
end;

theorem Th20:
for L be non empty HGrStr
for B be non empty AlgebraStr over L
for A be Subset of B st A is opers_closed ex C being strict Subalgebra of B
st the carrier of C = A
proof
 let L be non empty HGrStr;
 let B be non empty AlgebraStr over L;
 let A be Subset of B such that
A1: A is opers_closed;
A2: [:A,A:] c= [:the carrier of B,the carrier of B:] by ZFMISC_1:119;
 reconsider f1 = (the add of B)|[:A,A:] as Function;
    dom f1 = [:A,A:] & for x being set st x in [:A,A:] holds f1.x in A
   proof
       [:A,A:] c= dom the add of B by A2,Th1;
    hence dom f1 = [:A,A:] by RELAT_1:91;
    let x be set such that
A3:  x in [:A,A:];
    consider y,z be set such that
A4:  y in A & z in A & x = [y,z] by A3,ZFMISC_1:def 2;
    reconsider y,z as Element of B by A4;
A5:  A is lineary-closed by A1,Def4;
       f1.x = (the add of B).[y,z] by A3,A4,FUNCT_1:72
         .= y + z by RLVECT_1:def 3;
     hence f1.x in A by A4,A5,VECTSP_4:def 1;
    end;
 then reconsider ad = f1 as BinOp of A by FUNCT_2:5;
 reconsider f2 = (the mult of B)|[:A,A:] as Function;
      [:A,A:] c= dom the mult of B by A2,Th1;
then A6: dom f2 = [:A,A:] by RELAT_1:91;
    for x being set st x in [:A,A:] holds f2.x in A
   proof
    let x be set such that
A7:  x in [:A,A:];
    consider y,z be set such that
A8:  y in A & z in A & x = [y,z] by A7,ZFMISC_1:def 2;
    reconsider y,z as Element of B by A8;
       f2.x = (the mult of B).[y,z] by A7,A8,FUNCT_1:72
         .= (the mult of B).(y,z) by BINOP_1:def 1
         .= y * z by VECTSP_1:def 10;
    hence f2.x in A by A1,A8,Def4;
   end;
 then reconsider mu = f2 as BinOp of A by A6,FUNCT_2:5;
 reconsider f4 = (the lmult of B)|[:the carrier of L,A:] as Function;
      [:the carrier of L,A:] c= [:the carrier of L,the carrier of B:]
      by ZFMISC_1:119;
    then [:the carrier of L,A:] c= dom the lmult of B by Th2;
then A9: dom f4 = [:the carrier of L,A:] by RELAT_1:91;
    for x being set st x in [:the carrier of L,A:] holds f4.x in A
   proof
    let x be set such that
A10:  x in [:the carrier of L,A:];
    consider y,z be set such that
A11:  y in the carrier of L & z in A & x = [y,z] by A10,ZFMISC_1:def 2;
    reconsider y as Element of L by A11;
    reconsider z as Element of B by A11;
A12:  A is lineary-closed by A1,Def4;
       f4.x = (the lmult of B).[y,z] by A10,A11,FUNCT_1:72
         .= (the lmult of B).(y,z) by BINOP_1:def 1
         .= y * z by VECTSP_1:def 24;
    hence f4.x in A by A11,A12,VECTSP_4:def 1;
   end;
 then reconsider lm = f4 as Function of [:the carrier of L,A:],A by A9,FUNCT_2:
5;
    0.B in A by A1,Def4;
 then reconsider z = the Zero of B as Element of A by RLVECT_1:def 2;
    1_(B) in A by A1,Def4;
 then reconsider u = the unity of B as Element of A by VECTSP_1:def 9;
set c = AlgebraStr(# A, ad, mu, z, u, lm #);
A13: 1_(c) = the unity of c by VECTSP_1:def 9
         .= 1_(B) by VECTSP_1:def 9;
    0.c = the Zero of c by RLVECT_1:def 2
         .= 0.B by RLVECT_1:def 2;
 then reconsider C=c as strict Subalgebra of B by A13,Def3;
 take C;
 thus thesis;
end;

theorem Th21:
for L being non empty HGrStr
for B being non empty AlgebraStr over L
for A being non empty Subset of B
for X being Subset-Family of B st
(for Y be set holds Y in X iff Y c= the carrier of B &
   ex C being Subalgebra of B st Y = the carrier of C & A c= Y) holds
     meet X is opers_closed
 proof
  let L being non empty HGrStr;
  let B being non empty AlgebraStr over L;
  let A being non empty Subset of B;
  let X being Subset-Family of B such that
A1:  for Y be set holds Y in X iff Y c= the carrier of B &
   ex C being Subalgebra of B st Y = the carrier of C & A c= Y;
      B is Subalgebra of B by Th11;
then A2: X <> {} by A1;
   thus meet X is lineary-closed
    proof
    thus for x,y being Element of B st x in meet X & y in meet
X
       holds x + y in meet X
     proof
      let x,y be Element of B such that
A3:    x in meet X & y in meet X;
         now let Y be set;
        assume A4: Y in X;
        then consider C be Subalgebra of B such that
A5:      Y = the carrier of C & A c= Y by A1;
        consider a be set such that A6: a in A by XBOOLE_0:def 1;
        reconsider C as non empty Subalgebra of B by A5,A6,STRUCT_0:def 1;
        reconsider x' = x, y' = y as Element of B;
        reconsider x1 = x', y1 = y' as Element of C
             by A3,A4,A5,SETFAM_1:def 1;
           x + y = x1+ y1 by Th15;
        hence x + y in Y by A5;
       end;
       hence x + y in meet X by A2,SETFAM_1:def 1;
     end;
    thus for a being Element of L,
      v being Element of B st v in meet X holds a * v in meet X
     proof
      let a be Element of L,
       v be Element of B such that
A7:    v in meet X;
        now let Y be set;
       assume A8: Y in X;
       then consider C be Subalgebra of B such that
A9:     Y = the carrier of C & A c= Y by A1;
       consider z be set such that A10: z in A by XBOOLE_0:def 1;
       reconsider C as non empty Subalgebra of B by A9,A10,STRUCT_0:def 1;
       reconsider v' = v as Element of C
           by A7,A8,A9,SETFAM_1:def 1;
          a * v = a * v' by Th17;
      hence a * v in Y by A9;
      end;
      hence a * v in meet X by A2,SETFAM_1:def 1;
     end;
    end;
   thus for x,y being Element of B st x in meet X & y in meet X holds
    x*y in meet X
    proof
     let x,y be Element of B such that
A11:   x in meet X & y in meet X;
       now let Y be set;
      assume A12: Y in X;
      then consider C be Subalgebra of B such that
A13:    Y = the carrier of C & A c= Y by A1;
      consider a be set such that A14: a in A by XBOOLE_0:def 1;
      reconsider C as non empty Subalgebra of B by A13,A14,STRUCT_0:def 1;
      reconsider x' = x, y' = y as Element of B;
      reconsider x1 = x', y1 = y' as Element of C by A11,A12,A13
,SETFAM_1:def 1;
         x*y = x1* y1 by Th16;
      hence x*y in Y by A13;
     end;
     hence x*y in meet X by A2,SETFAM_1:def 1;
    end;
      now let Y be set;
     assume Y in X;
     then consider C be Subalgebra of B such that
A15:   Y = the carrier of C & A c= Y by A1;
      consider a be set such that A16: a in A by XBOOLE_0:def 1;
     reconsider C as non empty Subalgebra of B by A15,A16,STRUCT_0:def 1;
        1_(B) = 1_(C) by Def3;
      then 1_(B) in the carrier of C;
     hence 1_(B) in Y by A15;
    end;
   hence 1_(B) in meet X by A2,SETFAM_1:def 1;
      now let Y be set;
     assume Y in X;
     then consider C be Subalgebra of B such that
A17:   Y = the carrier of C & A c= Y by A1;
      consider a be set such that A18: a in A by XBOOLE_0:def 1;
     reconsider C as non empty Subalgebra of B by A17,A18,STRUCT_0:def 1;
        0.B = 0.C by Def3;
      then 0.B in the carrier of C;
     hence 0.B in Y by A17;
    end;
   hence 0.B in meet X by A2,SETFAM_1:def 1;
 end;

definition
let L be non empty HGrStr;
let B be non empty AlgebraStr over L;
let A be non empty Subset of B;
 func GenAlg A -> strict non empty Subalgebra of B means :Def5:
 A c= the carrier of it &
  for C being Subalgebra of B st A c= the carrier of C holds
   the carrier of it c= the carrier of C;
existence
 proof
  defpred P[set] means ex C being Subalgebra of B st
   $1 = the carrier of C & A c= $1;
  consider X be Subset-Family of B such that
A1: for Y being Subset of B holds Y in X iff P[Y] from SubFamEx;
    set M = meet X;
      B is Subalgebra of B by Th11;
then the carrier of B in bool the carrier of B & ex C being Subalgebra of B st
     the carrier of B = the carrier of C & A c= the carrier of B
     by ZFMISC_1:def 1;
then A2:  X <> {} by A1;
      for Y be set holds Y in X iff Y c= the carrier of B &
       ex C being Subalgebra of B st Y = the carrier of C & A c= Y by A1;
    then A3: M is opers_closed by Th21;
    then consider C being strict Subalgebra of B such that
A4: M = the carrier of C by Th20;
      the carrier of C is non empty by A3,A4,Def4;
    then reconsider C as non empty strict Subalgebra of B by STRUCT_0:def 1;
    take C;
      now let Y be set such that
A5:  Y in X;
       ex C being Subalgebra of B st Y = the carrier of C & A c= Y by A1,A5;
     hence A c= Y;
    end;
    hence A c= the carrier of C by A2,A4,SETFAM_1:6;
    let C1 be Subalgebra of B such that
A6:  A c= the carrier of C1;
       the carrier of C1 c= the carrier of B by Def3;
     then the carrier of C1 in X by A1,A6;
    hence the carrier of C c= the carrier of C1 by A4,SETFAM_1:4;
 end;
uniqueness
 proof
  let P1,P2 be strict non empty Subalgebra of B such that
A7: A c= the carrier of P1 and
A8: for C being Subalgebra of B st A c= the carrier of C holds
     the carrier of P1 c= the carrier of C and
A9: A c= the carrier of P2 and
A10: for C being Subalgebra of B st A c= the carrier of C holds
    the carrier of P2 c= the carrier of C;
A11: the carrier of P1 c= the carrier of P2 by A8,A9;
A12: the carrier of P2 c= the carrier of P1 by A7,A10;
then A13: the carrier of P1 = the carrier of P2 by A11,XBOOLE_0:def 10;
      now let x be Element of P1,
            y be Element of P2;
     reconsider x1=x as Element of P2 by A11,A12,XBOOLE_0:def 10
;
     reconsider y1=y as Element of P1 by A11,A12,XBOOLE_0:def 10
;
A14:  the carrier of P2 c= the carrier of B by Def3;
     then reconsider x' = x1 as Element of B by TARSKI:def 3;
     reconsider y' = y as Element of B by A14,TARSKI:def 3;
     thus (the add of P1).(x,y) = x + y1 by RLVECT_1:5
        .= x' + y' by Th15
        .= x1 + y by Th15
        .= (the add of P2).(x,y) by RLVECT_1:5;
    end;
then A15: the add of P1 = the add of P2 by A13,BINOP_1:2;
      now let x be Element of P1,
            y be Element of P2;
     reconsider x1=x as Element of P2 by A11,A12,XBOOLE_0:def 10
;
     reconsider y1=y as Element of P1 by A11,A12,XBOOLE_0:def 10
;
A16:  the carrier of P2 c= the carrier of B by Def3;
     then reconsider x' = x1 as Element of B by TARSKI:def 3;
     reconsider y' = y as Element of B by A16,TARSKI:def 3;
     thus (the mult of P1).(x,y) = x * y1 by VECTSP_1:def 10
        .= x' * y' by Th16
        .= x1 * y by Th16
        .= (the mult of P2).(x,y) by VECTSP_1:def 10;
    end;
then A17: the mult of P1 = the mult of P2 by A13,BINOP_1:2;
A18: the Zero of P1 = 0.P1 by RLVECT_1:def 2
        .= 0.B by Def3
        .= 0.P2 by Def3
        .= the Zero of P2 by RLVECT_1:def 2;
A19: the unity of P1 = 1_(P1) by VECTSP_1:def 9
        .= 1_(B) by Def3
        .= 1_(P2) by Def3
        .= the unity of P2 by VECTSP_1:def 9;
      now let x be Element of L,
            y be Element of P1;
     reconsider y1=y as Element of P2 by A11,A12,XBOOLE_0:def 10
;
       the carrier of P2 c= the carrier of B by Def3;
     then reconsider y' = y1 as Element of B by TARSKI:def 3;
     thus (the lmult of P1).(x,y) = x * y by VECTSP_1:def 24
        .= x * y' by Th17
        .= x * y1 by Th17
        .= (the lmult of P2).(x,y) by VECTSP_1:def 24;
    end;
  hence P1 = P2 by A13,A15,A17,A18,A19,BINOP_1:2;
 end;
end;

theorem Th22:
for L be non empty HGrStr
for B be non empty AlgebraStr over L
for A be non empty Subset of B st A is opers_closed holds
the carrier of GenAlg A = A
 proof
  let L be non empty HGrStr;
  let B be non empty AlgebraStr over L;
  let A be non empty Subset of B such that
A1: A is opers_closed;
A2: A c= the carrier of GenAlg A by Def5;
  consider C be strict Subalgebra of B such that A3: the carrier of C = A
   by A1,Th20;
     the carrier of GenAlg A c= A by A3,Def5;
  hence thesis by A2,XBOOLE_0:def 10;
 end;

begin ::The Algebra of Polynomials

definition
let L be add-associative right_zeroed right_complementable distributive
 (non empty doubleLoopStr);
func Polynom-Algebra L -> strict non empty AlgebraStr over L means
:Def6:
 ex A being non empty Subset of Formal-Series L st
  A = the carrier of Polynom-Ring L & it = GenAlg A;
 existence
  proof
    the carrier of Polynom-Ring L c= the carrier of Formal-Series L
   proof
    let x be set;
     assume x in the carrier of Polynom-Ring L;
      then x is AlgSequence of L by POLYNOM3:def 12;
    hence thesis by Def2;
   end;
  then reconsider A = the carrier of Polynom-Ring L as non empty Subset of
   Formal-Series L;
  take GenAlg A;
  thus thesis;
  end;
 uniqueness;
end;

definition
let L be add-associative right_zeroed right_complementable
 distributive (non empty doubleLoopStr);
cluster Polynom-Ring L -> Loop-like;
coherence
proof
   now thus for a,b be Element of Polynom-Ring L
        ex x being Element of Polynom-Ring L st a+x=b
         by RLVECT_1:20;
 thus for a,b be Element of Polynom-Ring L
        ex x being Element of Polynom-Ring L st x+a=b
  proof
   let a,b be Element of Polynom-Ring L;
    reconsider x = b - a as Element of Polynom-Ring L;
    take x;
    thus x + a = (b + (-a)) + a by RLVECT_1:def 11
              .= b + ((-a) + a) by RLVECT_1:def 6
              .= b + 0.(Polynom-Ring L) by RLVECT_1:16
              .= b by RLVECT_1:10;
  end;
 thus for a,x,y be Element of Polynom-Ring L holds a+x=a+y
         implies x=y by RLVECT_1:21;
 thus for a,x,y be Element of Polynom-Ring L holds x+a=y+a
         implies x=y by RLVECT_1:21;
 end;
 hence thesis by ALGSTR_1:7;
end;
end;

theorem Th23:
for L being add-associative right_zeroed right_complementable
  distributive (non empty doubleLoopStr)
for A being non empty Subset of Formal-Series L st
   A = the carrier of Polynom-Ring L holds A is opers_closed
 proof
  let L be add-associative right_zeroed right_complementable
  distributive (non empty doubleLoopStr);
  let A be non empty Subset of Formal-Series L such that
A1: A = the carrier of Polynom-Ring L;
   set B = Formal-Series L;
   thus A is lineary-closed
    proof
     thus for v,u being Element of B st v in A & u in A
       holds v + u in A
      proof
       let v,u be Element of B such that
A2:     v in A & u in A;
        reconsider p = v, q = u as AlgSequence of L by A1,A2,POLYNOM3:def 12;
          v + u = p + q by Def2;
       hence v + u in A by A1,POLYNOM3:def 12;
      end;
     thus for a being Element of L,
        v being Element of B
     st v in A holds a * v in A
      proof
       let a be Element of L,
           v being Element of B such that
A3:     v in A;
        reconsider a' = a as Element of L;
        reconsider p = v as AlgSequence of L by A1,A3,POLYNOM3:def 12;
          a * v = a' * p by Def2;
       hence a * v in A by A1,POLYNOM3:def 12;
      end;
    end;
   thus for u,v being Element of B st u in A & v in A holds u*v in A
    proof
     let u,v be Element of B such that
A4:   u in A & v in A;
     reconsider p = u,q = v as AlgSequence of L by A1,A4,POLYNOM3:def 12;
        u * v = p*'q by Def2;
     hence u * v in A by A1,POLYNOM3:def 12;
    end;
      1_(B) = 1_.(L) by Def2
         .= 1_(Polynom-Ring L) by POLYNOM3:def 12;
   hence 1_(B) in A by A1;
      0.B = 0_.(L) by Def2
       .= 0.(Polynom-Ring L) by POLYNOM3:def 12;
   hence 0.B in A by A1;
 end;

theorem
  for L be add-associative right_zeroed right_complementable
 distributive (non empty doubleLoopStr) holds
the doubleLoopStr of Polynom-Algebra L = Polynom-Ring L
proof
let L be add-associative right_zeroed right_complementable
 distributive (non empty doubleLoopStr);
 consider A being non empty Subset of Formal-Series L such that
A1: A = the carrier of Polynom-Ring L & Polynom-Algebra L = GenAlg A by Def6;
A2: A is opers_closed by A1,Th23;
then A3: the carrier of Polynom-Algebra L = the carrier of Polynom-Ring L
      by A1,Th22;
A4: the carrier of Polynom-Algebra L c= the carrier of Formal-Series L
       by A1,Def3;
A5: for x being Element of Polynom-Algebra L
    for y being Element of Polynom-Ring L holds
    (the add of Polynom-Algebra L).(x,y)=(the add of Polynom-Ring L).(x,y)
    proof let x be Element of Polynom-Algebra L,
            y be Element of Polynom-Ring L;
     reconsider x1=x as Element of Polynom-Ring L
      by A1,A2,Th22;
     reconsider y1=y as Element of Polynom-Algebra L
      by A1,A2,Th22;
     reconsider x'=x as Element of Formal-Series L
      by A4,TARSKI:def 3;
     reconsider y'=y1 as Element of Formal-Series L
      by A1,TARSKI:def 3;
     reconsider p=x as AlgSequence of L by A3,POLYNOM3:def 12;
     reconsider q=y as AlgSequence of L by POLYNOM3:def 12;
     thus (the add of Polynom-Algebra L).(x,y) = x+y1 by RLVECT_1:5
        .= x' + y' by A1,Th15
        .= p+q by Def2
        .= x1+y by POLYNOM3:def 12
        .= (the add of Polynom-Ring L).(x,y) by RLVECT_1:5;
    end;
      now let x be Element of Polynom-Algebra L,
            y be Element of Polynom-Ring L;
     reconsider x1=x as Element of Polynom-Ring L
      by A1,A2,Th22;
     reconsider y1=y as Element of Polynom-Algebra L
      by A1,A2,Th22;
     reconsider x'=x as Element of Formal-Series L
      by A4,TARSKI:def 3;
     reconsider y'=y1 as Element of Formal-Series L
      by A1,TARSKI:def 3;
     reconsider p=x as AlgSequence of L by A3,POLYNOM3:def 12;
     reconsider q=y as AlgSequence of L by POLYNOM3:def 12;
     thus (the mult of Polynom-Algebra L).(x,y) = x*y1 by VECTSP_1:def 10
        .= x' * y' by A1,Th16
        .= p*'q by Def2
        .= x1*y by POLYNOM3:def 12
        .= (the mult of Polynom-Ring L).(x,y) by VECTSP_1:def 10;
    end;
then A6: the mult of Polynom-Algebra L = the mult of Polynom-Ring L
  by A3,BINOP_1:2;
A7: the Zero of Polynom-Algebra L = 0.(Polynom-Algebra L) by RLVECT_1:def 2
       .= 0.(Formal-Series L) by A1,Def3
       .= 0_.(L) by Def2
       .= 0.(Polynom-Ring L) by POLYNOM3:def 12
       .= the Zero of Polynom-Ring L by RLVECT_1:def 2;
   the unity of Polynom-Algebra L = 1_(Polynom-Algebra L) by VECTSP_1:def 9
       .= 1_(Formal-Series L) by A1,Def3
       .= 1_.(L) by Def2
       .= 1_(Polynom-Ring L) by POLYNOM3:def 12
       .= the unity of Polynom-Ring L by VECTSP_1:def 9;
 hence thesis by A3,A5,A6,A7,BINOP_1:2;
end;


Back to top