:: Multivariate polynomials with arbitrary number of variables :: by Piotr Rudnicki and Andrzej Trybulec :: :: Received September 22, 1999 :: Copyright (c) 1999-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, ZFMISC_1, RLVECT_1, ALGSTR_0, VECTSP_1, XBOOLE_0, SUPINF_2, MESFUNC1, SUBSET_1, RELAT_1, FINSEQ_1, ARYTM_3, PARTFUN1, TARSKI, CARD_3, NAT_1, ORDINAL4, FUNCT_1, FVSUM_1, ALGSTR_1, BINOP_1, LATTICES, PRE_POLY, ALGSEQ_1, FINSET_1, ARYTM_1, FUNCOP_1, GROUP_1, FUNCT_4, ORDINAL1, XXREAL_0, FINSEQ_2, MEMBER_1, FUNCT_2, CARD_1, POLYNOM1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0, FUNCT_3, XCMPLX_0, XXREAL_0, BINOP_1, NAT_1, ALGSTR_1, RLVECT_1, FINSEQ_2, GROUP_1, VECTSP_1, FUNCOP_1, FUNCT_7, MATRLIN, VFUNCT_1, FVSUM_1, PRE_POLY, RECDEF_1; constructors BINOP_1, FINSEQOP, FINSEQ_4, RFUNCT_3, FUNCT_7, ALGSTR_1, FVSUM_1, MATRLIN, RECDEF_1, RELSET_1, PBOOLE, VFUNCT_1, GROUP_1, PRE_POLY; registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, CARD_1, MEMBERED, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, VALUED_0, PRE_POLY, RELSET_1, VFUNCT_1, FUNCT_2, ORDINAL1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin registration cluster degenerated -> trivial for add-associative right_zeroed right_complementable right_unital right-distributive non empty doubleLoopStr; end; registration cluster non trivial -> non degenerated for add-associative right_zeroed right_complementable right_unital right-distributive non empty doubleLoopStr; end; theorem :: POLYNOM1:1 for K being non empty addLoopStr, p1,p2 be FinSequence of the carrier of K st dom p1 = dom p2 holds dom(p1+p2) = dom p1; theorem :: POLYNOM1:2 for L being non empty addLoopStr, F being FinSequence of (the carrier of L)* holds dom Sum F = dom F; theorem :: POLYNOM1:3 for L being non empty addLoopStr, F being FinSequence of (the carrier of L)* holds Sum (<*>((the carrier of L)*)) = <*>(the carrier of L); theorem :: POLYNOM1:4 for L being non empty addLoopStr, p being Element of (the carrier of L)* holds <*Sum p*> = Sum<*p*>; theorem :: POLYNOM1:5 for L being non empty addLoopStr, F,G being FinSequence of (the carrier of L)* holds Sum(F^G) = Sum F ^ Sum G; definition let L be non empty multMagma, p be FinSequence of the carrier of L, a be Element of L; redefine func a*p means :: POLYNOM1:def 1 dom it = dom p & for i being object st i in dom p holds it/.i = a*(p/.i); end; definition let L be non empty multMagma, p be FinSequence of the carrier of L, a be Element of L; func p*a -> FinSequence of the carrier of L means :: POLYNOM1:def 2 dom it = dom p & for i being object st i in dom p holds it/.i = (p/.i)*a; end; theorem :: POLYNOM1:6 for L being non empty multMagma, a being Element of L holds a* <*>(the carrier of L) = <*>(the carrier of L); theorem :: POLYNOM1:7 for L being non empty multMagma, a being Element of L holds (<*> the carrier of L)*a = <*>(the carrier of L); theorem :: POLYNOM1:8 for L being non empty multMagma, a, b being Element of L holds a *<*b*> = <*a*b*>; theorem :: POLYNOM1:9 for L being non empty multMagma, a, b being Element of L holds <*b*>*a = <*b*a*>; theorem :: POLYNOM1:10 for L being non empty multMagma, a being Element of L, p, q being FinSequence of the carrier of L holds a*(p^q) = (a*p)^(a*q); theorem :: POLYNOM1:11 for L being non empty multMagma, a being Element of L, p, q being FinSequence of the carrier of L holds (p^q)*a = (p*a)^(q*a); registration cluster right_unital for non empty strict multLoopStr_0; end; registration cluster strict Abelian add-associative right_zeroed right_complementable associative commutative distributive almost_left_invertible well-unital non trivial for non empty doubleLoopStr; end; theorem :: POLYNOM1:12 for L being add-associative right_zeroed right_complementable right_unital distributive non empty doubleLoopStr, a being Element of L, p being FinSequence of the carrier of L holds Sum (a*p) = a*Sum p; theorem :: POLYNOM1:13 for L being add-associative right_zeroed right_complementable right_unital distributive non empty doubleLoopStr, a being Element of L, p being FinSequence of the carrier of L holds Sum (p*a) = (Sum p)*a; begin :: Sequence flattening -------------------------------------------------- theorem :: POLYNOM1:14 for L being add-associative right_zeroed right_complementable non empty addLoopStr, F being FinSequence of (the carrier of L)* holds Sum FlattenSeq F = Sum Sum F; definition let S be ZeroStr, f be (the carrier of S)-valued Function; func Support f -> set means :: POLYNOM1:def 3 for x being object holds x in it iff x in dom f & f.x <> 0.S; end; definition let X be non empty set, S be non empty ZeroStr, f be Function of X, S; redefine func Support f -> Subset of X means :: POLYNOM1:def 4 for x being Element of X holds x in it iff f.x <> 0.S; end; definition let S be ZeroStr, p be (the carrier of S)-valued Function; attr p is finite-Support means :: POLYNOM1:def 5 Support p is finite; end; definition let n be set, L be non empty 1-sorted, p be Function of Bags n, L, x be bag of n; redefine func p.x -> Element of L; end; begin :: Formal power series -------------------------------------------------- definition let X be set, S be 1-sorted; mode Series of X, S is Function of Bags X, S; end; definition let n be set, L be non empty addLoopStr, p,q be Series of n, L; func p+q -> Series of n, L equals :: POLYNOM1:def 6 p + q; end; theorem :: POLYNOM1:15 for n being set, L being non empty addLoopStr, p,q being Series of n, L for x being bag of n holds (p+q).x = p.x + q.x; theorem :: POLYNOM1:16 for n being set, L being non empty addLoopStr, p,q,r being Series of n, L st for x being bag of n holds r.x = p.x + q.x holds r = p + q; theorem :: POLYNOM1:17 for n being set, L being add-associative right_zeroed right_complementable non empty addLoopStr, p being Series of n, L for x being bag of n holds (-p).x = -(p.x); theorem :: POLYNOM1:18 for n being set, L being add-associative right_zeroed right_complementable non empty addLoopStr, p,r being Series of n, L st for x being bag of n holds r.x = -(p.x) holds r = -p; theorem :: POLYNOM1:19 for n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L holds p = - -p; theorem :: POLYNOM1:20 for n being set, L being right_zeroed non empty addLoopStr, p, q being Series of n, L holds Support (p+q) c= Support p \/ Support q; definition let n be set, L be Abelian right_zeroed non empty addLoopStr, p, q be Series of n, L; redefine func p+q; commutativity; end; theorem :: POLYNOM1:21 for n being set, L being add-associative right_zeroed non empty doubleLoopStr, p, q, r being Series of n, L holds (p+q)+r = p+(q+r); definition let n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p, q be Series of n, L; func p-q -> Series of n, L equals :: POLYNOM1:def 7 p+-q; end; definition let n be set, S be non empty ZeroStr; func 0_(n, S) -> Series of n, S equals :: POLYNOM1:def 8 (Bags n) --> 0.S; end; theorem :: POLYNOM1:22 for n being set, S being non empty ZeroStr, b be bag of n holds (0_(n, S)).b = 0.S; theorem :: POLYNOM1:23 for n being set, L be right_zeroed non empty addLoopStr, p be Series of n, L holds p+0_(n,L) = p; definition let n be set, L be right_unital non empty multLoopStr_0; func 1_(n,L) -> Series of n, L equals :: POLYNOM1:def 9 0_(n,L)+*(EmptyBag n,1.L); end; theorem :: POLYNOM1:24 for n being set, L being add-associative right_zeroed right_complementable non empty addLoopStr, p being Series of n, L holds p-p = 0_(n,L); theorem :: POLYNOM1:25 for n being set, L being right_unital non empty multLoopStr_0 holds (1_(n,L)).EmptyBag n = 1.L & for b being bag of n st b <> EmptyBag n holds (1_(n,L)).b = 0.L; definition let n be Ordinal, L be add-associative right_complementable right_zeroed non empty doubleLoopStr, p, q be Series of n, L; func p*'q -> Series of n, L means :: POLYNOM1:def 10 for b being bag of n ex s being FinSequence of the carrier of L st it.b = Sum s & len s = len decomp b & for k being Element of NAT st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2; end; theorem :: POLYNOM1:26 for n being Ordinal, L being Abelian add-associative right_zeroed right_complementable distributive associative non empty doubleLoopStr, p, q, r being Series of n, L holds p*'(q+r) = p*'q+p*'r; theorem :: POLYNOM1:27 for n being Ordinal, L being Abelian add-associative right_zeroed right_complementable right_unital distributive associative non empty doubleLoopStr, p, q, r being Series of n, L holds (p*'q)*'r = p*'(q*'r); definition let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative non empty doubleLoopStr, p, q be Series of n , L; redefine func p*'q; commutativity; end; theorem :: POLYNOM1:28 for n being Ordinal, L being add-associative right_complementable right_zeroed right_unital distributive non empty doubleLoopStr, p being Series of n, L holds p*'0_(n,L) = 0_(n,L); theorem :: POLYNOM1:29 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive right_unital non trivial non empty doubleLoopStr, p being Series of n, L holds p*'1_(n,L) = p; theorem :: POLYNOM1:30 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive well-unital non trivial non empty doubleLoopStr, p being Series of n, L holds 1_(n,L)*'p = p; begin :: Polynomials ---------------------------------------------------------- registration let n be set, S be non empty ZeroStr; cluster finite-Support for Series of n, S; end; definition let n be Ordinal, S be non empty ZeroStr; mode Polynomial of n, S is finite-Support Series of n, S; end; registration let n be Ordinal, L be right_zeroed non empty addLoopStr, p, q be Polynomial of n, L; cluster p+q -> finite-Support; end; registration let n be Ordinal, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L; cluster -p -> finite-Support; end; registration let n be Element of NAT, L be add-associative right_zeroed right_complementable non empty addLoopStr, p, q be Polynomial of n, L; cluster p-q -> finite-Support; end; registration let n be Ordinal, S be non empty ZeroStr; cluster 0_(n, S) -> finite-Support; end; registration let n be Ordinal, L be add-associative right_zeroed right_complementable right_unital right-distributive non trivial doubleLoopStr; cluster 1_(n,L) -> finite-Support; end; registration let n be Ordinal, L be add-associative right_complementable right_zeroed right_unital distributive non empty doubleLoopStr, p, q be Polynomial of n, L; cluster p*'q -> finite-Support; end; begin :: The ring of polynomials --------------------------------------------- definition let n be Ordinal, L be right_zeroed add-associative right_complementable right_unital distributive non trivial doubleLoopStr; func Polynom-Ring (n, L) -> strict non empty doubleLoopStr means :: POLYNOM1:def 11 ( for x being set holds x in the carrier of it iff x is Polynomial of n, L) & ( for x, y being Element of it, p, q being Polynomial of n, L st x = p & y = q holds x+y = p+q) & (for x, y being Element of it, p, q being Polynomial of n, L st x = p & y = q holds x*y = p*'q) & 0.it = 0_(n,L) & 1.it = 1_(n,L); end; registration let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable right_unital distributive non trivial doubleLoopStr; cluster Polynom-Ring (n, L) -> Abelian; end; registration let n be Ordinal, L be add-associative right_zeroed right_complementable right_unital distributive non trivial doubleLoopStr; cluster Polynom-Ring (n, L) -> add-associative; end; registration let n be Ordinal, L be right_zeroed add-associative right_complementable right_unital distributive non trivial doubleLoopStr; cluster Polynom-Ring (n, L) -> right_zeroed; end; registration let n be Ordinal, L be right_complementable right_zeroed add-associative right_unital distributive non trivial doubleLoopStr; cluster Polynom-Ring (n, L) -> right_complementable; end; registration let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative right_unital distributive non trivial non empty doubleLoopStr; cluster Polynom-Ring (n, L) -> commutative; end; registration let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable right_unital distributive associative non trivial non empty doubleLoopStr; cluster Polynom-Ring (n, L) -> associative; 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 right-distributive; end; theorem :: POLYNOM1:31 for n being Ordinal, L being right_zeroed Abelian add-associative right_complementable right_unital distributive associative non trivial non empty doubleLoopStr holds 1.Polynom-Ring(n, L) = 1_(n,L);