:: Evaluation of Multivariate Polynomials
::  by Christoph Schwarzweller and Andrzej Trybulec
::
:: Received April 14, 2000
:: Copyright (c) 2000-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, XBOOLE_0, SUBSET_1, FINSEQ_1, RELAT_1, PARTFUN1, CARD_1,
      FUNCT_1, TARSKI, XXREAL_0, ARYTM_1, ARYTM_3, NAT_1, ORDERS_1, RELAT_2,
      GROUP_1, BINOP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES, ZFMISC_1,
      FINSET_1, ALGSTR_1, STRUCT_0, SUPINF_2, CARD_3, FINSOP_1, ORDINAL4,
      PRE_POLY, FINSEQ_5, FUNCT_4, FUNCOP_1, ORDINAL1, WELLORD2, MESFUNC1,
      RFINSEQ, POLYNOM1, ALGSEQ_1, MSSUBFAM, QUOFIELD, POLYNOM2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      RELAT_1, FINSOP_1, RELAT_2, RELSET_1, FUNCT_1, FINSET_1, XCMPLX_0,
      PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_7, REAL_1, NAT_1, ALGSTR_1,
      ORDERS_1, FINSEQ_1, STRUCT_0, ALGSTR_0, RLVECT_1, FUNCOP_1, VFUNCT_1,
      VECTSP_1, GROUP_1, GROUP_4, QUOFIELD, FINSEQ_5, GRCAT_1, RFINSEQ,
      YELLOW_1, GROUP_6, XXREAL_0, RECDEF_1, PRE_POLY, POLYNOM1;
 constructors REAL_1, FINSOP_1, RFINSEQ, BINARITH, FINSEQ_5, GROUP_4, GRCAT_1,
      GROUP_6, MONOID_0, TRIANG_1, YELLOW_1, QUOFIELD, POLYNOM1, RECDEF_1,
      ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, DOMAIN_1, RINGCAT1;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0,
      NAT_1, INT_1, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, POLYNOM1,
      VALUED_0, CARD_1, SUBSET_1, PRE_POLY, RELAT_1, VFUNCT_1, FUNCT_2,
      FUNCT_1, PBOOLE, RINGCAT1;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

theorem :: POLYNOM2:1
  for L being unital associative non empty multMagma, a being Element of L,
    n,m being Element of NAT holds
  power(L).(a,n+m) = power(L).(a,n) * power(L).(a,m);

registration
  cluster Abelian right_zeroed add-associative right_complementable
    well-unital distributive commutative associative for non trivial
    doubleLoopStr;
end;

begin

::$CT

theorem :: POLYNOM2:3
  for L being left_zeroed right_zeroed non empty addLoopStr, p
  being FinSequence of the carrier of L, i being Element of NAT st i in dom p &
  for i9 being Element of NAT st i9 in dom p & i9 <> i holds p/.i9 = 0.L holds
  Sum p = p/.i;

theorem :: POLYNOM2:4
  for L being add-associative right_zeroed right_complementable
distributive well-unital non empty doubleLoopStr, p being FinSequence of the
  carrier of L st ex i being Element of NAT st i in dom p & p/.i = 0.L holds
  Product p = 0.L;

theorem :: POLYNOM2:5
  for L being Abelian add-associative non empty addLoopStr, a
being Element of L, p,q being FinSequence of the carrier of L st len p = len q
  & ex i being Element of NAT st i in dom p & q/.i = a + p/.i & for i9 being
  Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9 holds Sum q = a +
  Sum p;

theorem :: POLYNOM2:6
  for L being commutative associative non empty doubleLoopStr, a
being Element of L, p,q being FinSequence of the carrier of L st len p = len q
  & ex i being Element of NAT st i in dom p & q/.i = a * p/.i & for i9 being
Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9 holds Product q = a
  * Product p;

begin :: Evaluation of Bags -------------------------------------------------------

definition
::$CD
  let n be Ordinal, b be bag of n, L be well-unital non trivial
  doubleLoopStr, x be Function of n, L;
  func eval(b,x) -> Element of L means
:: POLYNOM2:def 2

  ex y being FinSequence of the carrier of L st
  len y = len SgmX(RelIncl n, support b) & it = Product y &
  for i being Element of NAT st 1 <= i & i <= len y holds
  y/.i = power(L).((x * SgmX(RelIncl n, support b))/.i,
          (b * SgmX(RelIncl n, support b))/.i);
end;

::$CT 7

theorem :: POLYNOM2:14
  for n being Ordinal, L being well-unital non trivial
  doubleLoopStr, x being Function of n, L holds eval(EmptyBag n,x) = 1.L;

theorem :: POLYNOM2:15
  for n being Ordinal, L being well-unital non trivial
  doubleLoopStr, u being set, b being bag of n st support b = {u} for x being
  Function of n, L holds eval(b,x) = power(L).(x.u,b.u);

theorem :: POLYNOM2:16
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive Abelian non trivial commutative
  associative non empty doubleLoopStr, b1,b2 being bag of n, x being Function
  of n, L holds eval(b1+b2,x) = eval(b1,x) * eval(b2,x);

begin :: Evaluation of Polynomials ------------------------------------------------

registration
  let n be Ordinal, L be add-associative right_zeroed right_complementable
  non empty addLoopStr, p,q be Polynomial of n, L;
  cluster p - q -> finite-Support;
end;

theorem :: POLYNOM2:17
  for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, n being Ordinal
  , p being Polynomial of n,L st Support p = {} holds p = 0_(n,L);

registration
  let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
  of n,L;
  cluster Support p -> finite;
end;

theorem :: POLYNOM2:18
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive non trivial
  doubleLoopStr, p being Polynomial of n,L holds BagOrder n linearly_orders
  Support p;

definition
::$CD
  let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
  of n,L, x be Function of n, L;
  func eval(p,x) -> Element of L means
:: POLYNOM2:def 4

  ex y being FinSequence of the
  carrier of L st len y = len SgmX(BagOrder n, Support p) & it = Sum y & for i
being Element of NAT st 1 <= i & i <= len y holds y/.i = (p * SgmX(BagOrder n,
  Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x);
end;

theorem :: POLYNOM2:19
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L, b being bag of n st Support p = {b}
  for x being Function of n, L holds eval(p,x) = p.b * eval(b,x);

theorem :: POLYNOM2:20
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive non trivial
  doubleLoopStr, x being Function of n, L holds eval(0_(n,L),x) = 0.L;

theorem :: POLYNOM2:21
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive non trivial
  doubleLoopStr, x being Function of n, L holds eval(1_(n,L),x) = 1.L;

theorem :: POLYNOM2:22
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L, x being Function of n, L holds eval(
  -p,x) = - eval(p,x);

theorem :: POLYNOM2:23
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable Abelian well-unital distributive non trivial
  doubleLoopStr, p,q being Polynomial of n,L, x being Function of n, L holds
  eval(p+q,x) = eval(p,x) + eval(q,x);

theorem :: POLYNOM2:24
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable Abelian well-unital distributive non trivial
  doubleLoopStr, p,q being Polynomial of n,L, x being Function of n, L holds
  eval(p-q,x) = eval(p,x) - eval(q,x);

theorem :: POLYNOM2:25
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable Abelian well-unital distributive non trivial commutative
  associative non empty doubleLoopStr, p,q being Polynomial of n,L, x being
  Function of n, L holds eval(p*'q,x) = eval(p,x) * eval(q,x);

begin :: Evaluation Homomorphism --------------------------------------------------

definition
  let n be Ordinal, L be right_zeroed add-associative right_complementable
  well-unital distributive non trivial doubleLoopStr, x be Function
  of n, L;
  func Polynom-Evaluation(n,L,x) -> Function of Polynom-Ring(n,L),L means
:: POLYNOM2:def 5

   for p being Polynomial of n,L holds it.p = eval(p,x);
end;

registration
  let n be Ordinal, L be right_zeroed Abelian add-associative
  right_complementable well-unital distributive associative non trivial non
  empty doubleLoopStr;
  cluster Polynom-Ring (n, L) -> well-unital;
end;

registration
  let n be Ordinal, L be Abelian right_zeroed add-associative
  right_complementable well-unital distributive associative non trivial non
  empty doubleLoopStr, x be Function of n, L;
  cluster Polynom-Evaluation(n,L,x) -> unity-preserving;
end;

registration
  let n be Ordinal, L be right_zeroed add-associative right_complementable
  Abelian well-unital distributive non trivial doubleLoopStr, x be
  Function of n, L;
  cluster Polynom-Evaluation(n,L,x) -> additive;
end;

registration
  let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
  doubleLoopStr, x be Function of n, L;
  cluster Polynom-Evaluation(n,L,x) -> multiplicative;
end;

registration
  let n be Ordinal, L be right_zeroed add-associative right_complementable
  Abelian well-unital distributive commutative associative non trivial
  doubleLoopStr, x be Function of n, L;
  cluster Polynom-Evaluation(n,L,x) -> RingHomomorphism;
end;