:: The Algebra of Polynomials
::  by Ewa Gr\c{a}dzka
::
:: Received February 24, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, FUNCSDOM, BINOP_1,
      SUBSET_1, FUNCT_1, ZFMISC_1, XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1,
      GROUP_1, LATTICES, MESFUNC1, NAT_1, ARYTM_3, SUPINF_2, POLYNOM3,
      RLVECT_1, ARYTM_1, ALGSTR_1, FINSEQ_1, PARTFUN1, CARD_3, REALSET1,
      TARSKI, UNIALG_2, RLSUB_1, SETFAM_1, POLYNOM1, ALGSEQ_1, POLYALG1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS,
      XCMPLX_0, REALSET1, STRUCT_0, ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, FUNCOP_1, FINSEQ_1, BINOP_1, NAT_D, GROUP_1, RLVECT_1, VFUNCT_1,
      VECTSP_1, NORMSP_1, POLYNOM1, ALGSTR_1, ALGSEQ_1, POLYNOM3, POLYNOM5,
      VECTSP_4, XXREAL_0;
 constructors BINOP_1, REALSET1, RFINSEQ, NAT_D, ALGSTR_1, VECTSP_4, POLYNOM3,
      POLYNOM5, REAL_1, RELSET_1, FUNCOP_1, FVSUM_1, VFUNCT_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, NAT_1, REALSET1,
      STRUCT_0, VECTSP_1, FVSUM_1, POLYNOM3, POLYNOM5, BINOM, ORDINAL1,
      VFUNCT_1, FUNCT_2, RELAT_1;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

definition
  let F be 1-sorted;
  struct (doubleLoopStr,ModuleStr over F) AlgebraStr over F
  (# carrier -> set,
 addF, multF -> BinOp of the carrier,
 ZeroF, OneF -> Element of the carrier,
       lmult -> Function of [:the carrier of F,the carrier:], the carrier #);
end;

registration
  let L be non empty doubleLoopStr;
  cluster strict non empty for AlgebraStr over L;
end;

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

registration
  let L be non empty doubleLoopStr;
  cluster unital distributive vector-distributive scalar-distributive
  scalar-associative scalar-unital mix-associative for non empty
    AlgebraStr over L;
end;

definition
  let L be non empty doubleLoopStr;
  mode Algebra of L is unital distributive vector-distributive
  scalar-distributive scalar-associative scalar-unital mix-associative
    non empty AlgebraStr over L;
end;

theorem :: POLYALG1:1
  for X,Y being set for f being Function of [:X,Y:],X holds dom f = [:X,Y:];

theorem :: POLYALG1:2
  for X,Y being set for f being Function of [:X,Y:],Y holds dom f = [:X,Y:];

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
:: POLYALG1:def 2

  (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;
end;

registration
  let L be Abelian non empty doubleLoopStr;
  cluster Formal-Series L -> Abelian;
end;

registration
  let L be add-associative non empty doubleLoopStr;
  cluster Formal-Series L -> add-associative;
end;

registration
  let L be right_zeroed non empty doubleLoopStr;
  cluster Formal-Series L -> right_zeroed;
end;

registration
  let L be add-associative right_zeroed right_complementable non empty
  doubleLoopStr;
  cluster Formal-Series L -> right_complementable;
end;

registration
  let L be Abelian add-associative right_zeroed commutative non empty
  doubleLoopStr;
  cluster Formal-Series L -> commutative;
end;

registration
  let L be Abelian add-associative right_zeroed right_complementable
  well-unital associative distributive non empty doubleLoopStr;
  cluster Formal-Series L -> associative;
end;

registration
  cluster add-associative associative right_zeroed left_zeroed well-unital
    right_complementable distributive for non empty doubleLoopStr;
end;

::$CT 3


registration
  let L be right_zeroed add-associative right_complementable distributive
  well-unital non empty doubleLoopStr;
  cluster Formal-Series L -> well-unital;
end;

registration
  let L be Abelian add-associative right_zeroed right_complementable
  distributive non empty doubleLoopStr;
  cluster Formal-Series L -> right-distributive;
  cluster Formal-Series L -> left-distributive;
end;

theorem :: POLYALG1:6
  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;

theorem :: POLYALG1:7
  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;

theorem :: POLYALG1:8
  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);

theorem :: POLYALG1:9
  for L be associative well-unital non empty doubleLoopStr for p
  being sequence of L holds 1.L*p = p;

registration
  let L be Abelian add-associative associative right_zeroed
  right_complementable well-unital distributive non empty doubleLoopStr;
  cluster Formal-Series L -> vector-distributive scalar-distributive
    scalar-associative scalar-unital;
end;

theorem :: POLYALG1:10
  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;

registration
  let L be Abelian left_zeroed add-associative associative right_zeroed
  right_complementable distributive non empty doubleLoopStr;
  cluster Formal-Series L -> mix-associative;
end;

definition
  let L be 1-sorted;
  let A be AlgebraStr over L;
  mode Subalgebra of A -> AlgebraStr over L means
:: POLYALG1:def 3
    the carrier of it c= the carrier of A &
    1.it = 1.A & 0.it = 0.A &
    the addF of it = (the addF of A)||the carrier of it &
    the multF of it = (the multF of A)||the carrier of it &
    the lmult of it =
      (the lmult of A)|[:the carrier of L,the carrier of it:];
end;

theorem :: POLYALG1:11
  for L being 1-sorted for A being AlgebraStr over L holds A is Subalgebra of A
;

theorem :: POLYALG1:12
  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;

theorem :: POLYALG1:13
  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;

theorem :: POLYALG1:14
  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;

registration
  let L be non empty 1-sorted;
  cluster non empty strict for AlgebraStr over L;
end;

registration
  let L be 1-sorted;
  let B be AlgebraStr over L;
  cluster strict for Subalgebra of B;
end;

registration
  let L be non empty 1-sorted;
  let B be non empty AlgebraStr over L;
  cluster strict non empty for Subalgebra of B;
end;

definition
  let L be non empty multMagma;
  let B be non empty AlgebraStr over L;
  let A be Subset of B;
  attr A is opers_closed means
:: POLYALG1:def 4

  A is linearly-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 :: POLYALG1:15
  for L being non empty multMagma for B being non empty AlgebraStr
over L for A being non empty Subalgebra of B holds for x,y being Element of B,
  x9,y9 being Element of A st x = x9 & y = y9 holds x+y = x9+ y9;

theorem :: POLYALG1:16
  for L be non empty multMagma for B be non empty AlgebraStr over
  L for A be non empty Subalgebra of B holds for x,y being Element of B, x9,y9
  being Element of A st x = x9 & y = y9 holds x*y = x9* y9;

theorem :: POLYALG1:17
  for L be non empty multMagma 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, x9 being Element of A st x = x9 holds a * x = a * x9;

theorem :: POLYALG1:18
  for L be non empty multMagma 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;

theorem :: POLYALG1:19
  for L be non empty multMagma 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;

theorem :: POLYALG1:20
  for L being non empty multMagma 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;

definition
  let L be non empty multMagma;
  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
:: POLYALG1:def 5

  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;
end;

theorem :: POLYALG1:21
  for L be non empty multMagma 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;

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
:: POLYALG1:def 6

  ex
A being non empty Subset of Formal-Series L st A = the carrier of Polynom-Ring
  L & it = GenAlg A;
end;

registration
  let L be add-associative right_zeroed right_complementable distributive non
  empty doubleLoopStr;
  cluster Polynom-Ring L -> Loop-like;
end;

theorem :: POLYALG1:22
  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;

theorem :: POLYALG1:23
  for L be add-associative right_zeroed right_complementable
  distributive non empty doubleLoopStr holds the doubleLoopStr of
  Polynom-Algebra L = Polynom-Ring L;

theorem :: POLYALG1:24
  for L being add-associative right_zeroed right_complementable
  well-unital distributive non empty doubleLoopStr holds 1_Formal-Series L =
  1_.L;