:: More About Polynomials: Monomials and Constant Polynomials :: by Christoph Schwarzweller :: :: Received November 28, 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 RLVECT_1, ALGSTR_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES, VECTSP_2, ZFMISC_1, XBOOLE_0, STRUCT_0, POLYNOM1, VALUED_0, SUBSET_1, SUPINF_2, FUNCT_4, PRE_POLY, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL1, CARD_1, PARTFUN1, POLYNOM2, FINSEQ_1, CARD_3, NUMBERS, XXREAL_0, FINSET_1, ORDERS_1, ARYTM_3, NAT_1, MESFUNC1, QUOFIELD, GROUP_1, TARSKI, MSSUBFAM, ALGSEQ_1, CAT_3, XCMPLX_0, ORDINAL4, POLYNOM7, FUNCT_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_7, POLYNOM1, NUMBERS, XXREAL_0, DOMAIN_1, STRUCT_0, ALGSTR_0, FUNCT_4, NAT_1, ALGSTR_1, RLVECT_1, ORDERS_1, FINSEQ_1, FUNCOP_1, GROUP_1, QUOFIELD, GRCAT_1, VECTSP_2, POLYNOM2, VECTSP_1, GROUP_6, PRE_POLY; constructors REALSET2, GRCAT_1, GROUP_6, TRIANG_1, QUOFIELD, POLYNOM2, ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, FUNCT_4, RINGCAT1, MOD_4; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1, POLYNOM2, ALGSTR_0, CARD_1, SUBSET_1, PRE_POLY, FUNCT_1, RINGCAT1, MOD_4; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin registration cluster Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive domRing-like for non trivial doubleLoopStr; end; definition let X be set, R be non empty ZeroStr, p be Series of X,R; attr p is non-zero means :: POLYNOM7:def 1 p <> 0_(X,R); end; registration let X be set, R be non trivial ZeroStr; cluster non-zero for Series of X,R; end; registration let n be Ordinal, R be non trivial ZeroStr; cluster non-zero for Polynomial of n,R; end; theorem :: POLYNOM7:1 for X being set, R being non empty ZeroStr, s being Series of X,R holds s = 0_(X,R) iff Support s = {}; theorem :: POLYNOM7:2 for X being set, R being non empty ZeroStr holds R is non trivial iff ex s being Series of X,R st Support(s) <> {}; definition let X be set, b be bag of X; attr b is univariate means :: POLYNOM7:def 2 ex u being Element of X st support b = {u}; end; registration let X be non empty set; cluster univariate for bag of X; end; registration let X be non empty set; cluster univariate -> non empty-yielding for bag of X; end; begin :: Polynomials without Variables theorem :: POLYNOM7:3 for b being bag of {} holds b = EmptyBag {}; theorem :: POLYNOM7:4 for L being right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p being Polynomial of {}, L, x being Function of {},L holds eval(p,x) = p.(EmptyBag{}); theorem :: POLYNOM7:5 for L being right_zeroed add-associative right_complementable Abelian well-unital distributive associative non trivial non trivial doubleLoopStr holds Polynom-Ring({},L) is_ringisomorph_to L; begin :: Monomials definition let X be set, L be non empty ZeroStr, p be Series of X,L; attr p is monomial-like means :: POLYNOM7:def 3 ex b being bag of X st for b9 being bag of X st b9 <> b holds p.b9 = 0.L; end; registration let X be set, L be non empty ZeroStr; cluster monomial-like for Series of X,L; end; definition let X be set, L be non empty ZeroStr; mode Monomial of X,L is monomial-like Series of X,L; end; registration let X be set, L be non empty ZeroStr; cluster monomial-like -> finite-Support for Series of X,L; end; theorem :: POLYNOM7:6 for X being set, L being non empty ZeroStr, p being Series of X,L holds p is Monomial of X,L iff (Support p = {} or ex b being bag of X st Support p = {b}); definition let X be set, L be non empty ZeroStr, a be Element of L, b be bag of X; func Monom(a,b) -> Monomial of X,L equals :: POLYNOM7:def 4 0_(X,L)+*(b,a); end; definition let X be set, L be non empty ZeroStr, m be Monomial of X,L; func term(m) -> bag of X means :: POLYNOM7:def 5 m.it <> 0.L or Support m = {} & it = EmptyBag X; end; definition let X be set, L be non empty ZeroStr, m be Monomial of X,L; func coefficient(m) -> Element of L equals :: POLYNOM7:def 6 m.(term(m)); end; theorem :: POLYNOM7:7 for X being set, L being non empty ZeroStr, m being Monomial of X ,L holds Support(m) = {} or Support(m) = {term(m)}; theorem :: POLYNOM7:8 for X being set, L being non empty ZeroStr, b being bag of X holds coefficient(Monom(0.L,b)) = 0.L & term(Monom(0.L,b)) = EmptyBag X; theorem :: POLYNOM7:9 for X being set, L being non empty ZeroStr, a being Element of L, b being bag of X holds coefficient(Monom(a,b)) = a; theorem :: POLYNOM7:10 for X being set, L being non trivial ZeroStr, a being non zero Element of L, b being bag of X holds term(Monom(a,b)) = b; theorem :: POLYNOM7:11 for X being set, L being non empty ZeroStr, m being Monomial of X,L holds Monom(coefficient(m),term(m)) = m; theorem :: POLYNOM7:12 for n being Ordinal, L being right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, m being Monomial of n,L, x being Function of n,L holds eval(m,x) = coefficient(m) * eval(term(m),x); theorem :: POLYNOM7:13 for n being Ordinal, L being right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, a being Element of L, b being bag of n, x being Function of n,L holds eval(Monom( a,b),x) = a * eval(b,x); begin :: Constant Polynomials definition let X be set, L be non empty ZeroStr, p be Series of X,L; attr p is Constant means :: POLYNOM7:def 7 for b being bag of X st b <> EmptyBag X holds p.b = 0.L; end; registration let X be set, L be non empty ZeroStr; cluster Constant for Series of X,L; end; definition let X be set, L be non empty ZeroStr; mode ConstPoly of X,L is Constant Series of X,L; end; registration let X be set, L be non empty ZeroStr; cluster Constant -> monomial-like for Series of X,L; end; theorem :: POLYNOM7:14 for X being set, L being non empty ZeroStr, p being Series of X, L holds p is ConstPoly of X,L iff (p = 0_(X,L) or Support p = {EmptyBag X}); registration let X be set, L be non empty ZeroStr; cluster 0_(X,L) -> Constant; end; registration let X be set, L be well-unital non empty doubleLoopStr; cluster 1_(X,L) -> Constant; end; theorem :: POLYNOM7:15 for X being set, L being non empty ZeroStr, c being ConstPoly of X,L holds Support(c) = {} or Support(c) = {EmptyBag X}; theorem :: POLYNOM7:16 for X being set, L being non empty ZeroStr, c being ConstPoly of X,L holds term(c) = EmptyBag X & coefficient(c) = c.(EmptyBag X); definition let X be set, L be non empty ZeroStr, a be Element of L; func a |(X,L) -> Series of X,L equals :: POLYNOM7:def 8 0_(X,L)+*(EmptyBag X,a); end; registration let X be set, L be non empty ZeroStr, a be Element of L; cluster a |(X,L) -> Constant; end; theorem :: POLYNOM7:17 for X being set, L being non empty ZeroStr, p being Series of X,L holds p is ConstPoly of X,L iff ex a being Element of L st p = a |(X,L); theorem :: POLYNOM7:18 for X being set, L being non empty multLoopStr_0, a being Element of L holds (a |(X,L)).EmptyBag X = a & for b being bag of X st b <> EmptyBag X holds (a |(X,L)).b = 0.L; theorem :: POLYNOM7:19 for X being set, L being non empty ZeroStr holds 0.L |(X,L) = 0_(X,L); theorem :: POLYNOM7:20 for X being set, L being well-unital non empty multLoopStr_0 holds ( 1.L) |(X,L) = 1_(X,L); theorem :: POLYNOM7:21 for X being set, L being non empty ZeroStr, a,b being Element of L holds a |(X,L) = b |(X,L) iff a = b; theorem :: POLYNOM7:22 for X being set, L being non empty ZeroStr, a being Element of L holds Support(a |(X,L)) = {} or Support(a |(X,L)) = {EmptyBag X}; theorem :: POLYNOM7:23 for X being set, L being non empty ZeroStr, a being Element of L holds term(a |(X,L)) = EmptyBag X & coefficient(a |(X,L)) = a; theorem :: POLYNOM7:24 for n being Ordinal, L being right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, c being ConstPoly of n,L, x being Function of n,L holds eval(c,x) = coefficient(c ); theorem :: POLYNOM7:25 for n being Ordinal, L being right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, a being Element of L, x being Function of n,L holds eval(a |(n,L),x) = a; begin :: Multiplication with Coefficients definition let X be set, L be non empty multLoopStr_0, p be Series of X,L, a be Element of L; func a * p -> Series of X,L means :: POLYNOM7:def 9 for b being bag of X holds it.b = a * p.b; func p * a -> Series of X,L means :: POLYNOM7:def 10 for b being bag of X holds it.b = p.b * a; end; registration let X be set, L be left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr, p be finite-Support Series of X,L, a be Element of L; cluster a * p -> finite-Support; cluster p * a -> finite-Support; end; theorem :: POLYNOM7:26 for X being set, L being commutative non empty multLoopStr_0, p being Series of X,L, a being Element of L holds a * p = p * a; theorem :: POLYNOM7:27 for n being Ordinal, L being add-associative right_complementable right_zeroed left-distributive non empty doubleLoopStr, p being Series of n,L, a being Element of L holds a * p = a |(n,L) *' p; theorem :: POLYNOM7:28 for n being Ordinal, L being add-associative right_complementable right_zeroed right-distributive non empty doubleLoopStr, p being Series of n,L, a being Element of L holds p * a = p *' (a |(n,L)); theorem :: POLYNOM7:29 for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L, x being Function of n,L holds eval(a*p,x) = a * eval(p,x); theorem :: POLYNOM7:30 for n being Ordinal, L being left_zeroed right_zeroed left_add-cancelable add-associative right_complementable well-unital associative domRing-like distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L, x being Function of n,L holds eval(a*p ,x) = a * eval(p,x); theorem :: POLYNOM7:31 for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L, x being Function of n,L holds eval(p*a,x) = eval(p,x) * a; theorem :: POLYNOM7:32 for n being Ordinal, L being left_zeroed right_zeroed left_add-cancelable add-associative right_complementable well-unital associative commutative distributive domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L, x being Function of n,L holds eval(p*a,x) = eval(p,x) * a; theorem :: POLYNOM7:33 for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L, x being Function of n,L holds eval((a |(n,L))*'p,x) = a * eval(p, x); theorem :: POLYNOM7:34 for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being Element of L, x being Function of n,L holds eval(p*'(a |(n,L)),x) = eval(p,x) * a;