:: Evaluation of Multivariate Polynomials :: by Christoph Schwarzweller and Andrzej Trybulec :: :: Received April 14, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin Lm1: for X being set for A being Subset of X for O being Order of X holds ( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A ) proofend; Lm2: for X being set for A being Subset of X for O being Order of X st O is_connected_in X holds O is_connected_in A proofend; Lm3: for X being set for S being Subset of X for R being Order of X st R is being_linear-order holds R linearly_orders S proofend; theorem Th1: :: POLYNOM2:1 for L being non empty unital associative multMagma for a being Element of L for n, m being Element of NAT holds (power L) . (a,(n + m)) = ((power L) . (a,n)) * ((power L) . (a,m)) proofend; registration cluster non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive for doubleLoopStr ; existence ex b1 being non trivial doubleLoopStr st ( b1 is Abelian & b1 is right_zeroed & b1 is add-associative & b1 is right_complementable & b1 is well-unital & b1 is distributive & b1 is commutative & b1 is associative ) proofend; end; begin theorem Th2: :: POLYNOM2:2 for p being FinSequence for k being Element of NAT st k in dom p holds for i being Element of NAT st 1 <= i & i <= k holds i in dom p proofend; Lm4: for X being set for A being finite Subset of X for a being Element of X for R being Order of X st R linearly_orders {a} \/ A holds R linearly_orders A proofend; theorem Th3: :: POLYNOM2:3 for L being non empty right_zeroed left_zeroed addLoopStr for p being FinSequence of the carrier of L for 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 proofend; theorem :: POLYNOM2:4 for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for 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 proofend; theorem Th5: :: POLYNOM2:5 for L being non empty Abelian add-associative addLoopStr for a being Element of L for 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) proofend; theorem Th6: :: POLYNOM2:6 for L being non empty associative commutative doubleLoopStr for a being Element of L for 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) proofend; theorem Th7: :: POLYNOM2:7 for X being set for A being empty Subset of X for R being Order of X st R linearly_orders A holds SgmX (R,A) = {} proofend; theorem Th8: :: POLYNOM2:8 for X being set for A being finite Subset of X for R being Order of X st R linearly_orders A holds for i, j being Element of NAT st i in dom (SgmX (R,A)) & j in dom (SgmX (R,A)) & (SgmX (R,A)) /. i = (SgmX (R,A)) /. j holds i = j proofend; Lm5: for D being set for p being FinSequence of D st dom p <> {} holds 1 in dom p proofend; theorem Th9: :: POLYNOM2:9 for X being set for A being finite Subset of X for a being Element of X st not a in A holds for B being finite Subset of X st B = {a} \/ A holds for R being Order of X st R linearly_orders B holds for k being Element of NAT st k in dom (SgmX (R,B)) & (SgmX (R,B)) /. k = a holds for i being Element of NAT st 1 <= i & i <= k - 1 holds (SgmX (R,B)) /. i = (SgmX (R,A)) /. i proofend; theorem Th10: :: POLYNOM2:10 for X being set for A being finite Subset of X for a being Element of X st not a in A holds for B being finite Subset of X st B = {a} \/ A holds for R being Order of X st R linearly_orders B holds for k being Element of NAT st k in dom (SgmX (R,B)) & (SgmX (R,B)) /. k = a holds for i being Element of NAT st k <= i & i <= len (SgmX (R,A)) holds (SgmX (R,B)) /. (i + 1) = (SgmX (R,A)) /. i proofend; theorem Th11: :: POLYNOM2:11 for X being non empty set for A being finite Subset of X for a being Element of X st not a in A holds for B being finite Subset of X st B = {a} \/ A holds for R being Order of X st R linearly_orders B holds for k being Element of NAT st k + 1 in dom (SgmX (R,B)) & (SgmX (R,B)) /. (k + 1) = a holds SgmX (R,B) = Ins ((SgmX (R,A)),k,a) proofend; begin theorem Th12: :: POLYNOM2:12 for X being set for b being bag of X st support b = {} holds b = EmptyBag X proofend; Lm6: for X being set for b being bag of X holds b is PartFunc of X,NAT proofend; definition let X be set ; let b be bag of X; attrb is empty means :Def1: :: POLYNOM2:def 1 b = EmptyBag X; end; :: deftheorem Def1 defines empty POLYNOM2:def_1_:_ for X being set for b being bag of X holds ( b is empty iff b = EmptyBag X ); registration let X be non empty set ; cluster Relation-like X -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support non empty for set ; existence not for b1 being bag of X holds b1 is empty proofend; end; definition let X be set ; let b be bag of X; :: original:support redefine func support b -> finite Subset of X; coherence support b is finite Subset of X proofend; end; theorem Th13: :: POLYNOM2:13 for n being Ordinal for b being bag of n holds RelIncl n linearly_orders support b proofend; definition let X be set ; let x be FinSequence of X; let b be bag of X; :: original:* redefine funcb * x -> PartFunc of NAT,NAT; coherence x * b is PartFunc of NAT,NAT proofend; end; definition let n be Ordinal; let b be bag of n; let L be non trivial well-unital doubleLoopStr ; let x be Function of n,L; func eval (b,x) -> Element of L means :Def2: :: 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)) ) ); existence ex b1 being Element of L ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((RelIncl n),(support b))) & b1 = 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)) ) ) proofend; uniqueness for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((RelIncl n),(support b))) & b1 = 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)) ) ) & ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((RelIncl n),(support b))) & b2 = 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)) ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines eval POLYNOM2:def_2_:_ for n being Ordinal for b being bag of n for L being non trivial well-unital doubleLoopStr for x being Function of n,L for b5 being Element of L holds ( b5 = eval (b,x) iff ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((RelIncl n),(support b))) & b5 = 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)) ) ) ); Lm7: for X being set holds support (EmptyBag X) = {} proofend; theorem Th14: :: POLYNOM2:14 for n being Ordinal for L being non trivial well-unital doubleLoopStr for x being Function of n,L holds eval ((EmptyBag n),x) = 1. L proofend; theorem Th15: :: POLYNOM2:15 for n being Ordinal for L being non trivial well-unital doubleLoopStr for u being set for b being bag of n st support b = {u} holds for x being Function of n,L holds eval (b,x) = (power L) . ((x . u),(b . u)) proofend; Lm8: for n being Ordinal for L being non empty non trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr for b1, b2 being bag of n for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being set st u9 <> u holds b2 . u9 = b1 . u9 ) holds for x being Function of n,L for a being Element of L st a = (power L) . ((x . u),(b2 . u)) holds eval (b2,x) = a * (eval (b1,x)) proofend; Lm9: for n being Ordinal for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for b1 being bag of n st ex u being set st support b1 = {u} holds for b2 being bag of n for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x)) proofend; theorem Th16: :: POLYNOM2:16 for n being Ordinal for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for b1, b2 being bag of n for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x)) proofend; begin registration let n be Ordinal; let L be non empty right_complementable add-associative right_zeroed addLoopStr ; let p, q be Polynomial of n,L; clusterp - q -> finite-Support ; coherence p - q is finite-Support proofend; end; theorem Th17: :: POLYNOM2:17 for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for n being Ordinal for p being Polynomial of n,L st Support p = {} holds p = 0_ (n,L) proofend; registration let n be Ordinal; let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; let p be Polynomial of n,L; cluster Support p -> finite ; coherence Support p is finite by POLYNOM1:def_4; end; theorem Th18: :: POLYNOM2:18 for n being Ordinal for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for p being Polynomial of n,L holds BagOrder n linearly_orders Support p proofend; definition let n be Ordinal; let b be Element of Bags n; funcb @ -> bag of n equals :: POLYNOM2:def 3 b; correctness coherence b is bag of n; ; end; :: deftheorem defines @ POLYNOM2:def_3_:_ for n being Ordinal for b being Element of Bags n holds b @ = b; definition let n be Ordinal; let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; let p be Polynomial of n,L; let x be Function of n,L; func eval (p,x) -> Element of L means :Def4: :: 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)) ) ); existence ex b1 being Element of L ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((BagOrder n),(Support p))) & b1 = 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)) ) ) proofend; uniqueness for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((BagOrder n),(Support p))) & b1 = 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)) ) ) & ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((BagOrder n),(Support p))) & b2 = 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)) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines eval POLYNOM2:def_4_:_ for n being Ordinal for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for p being Polynomial of n,L for x being Function of n,L for b5 being Element of L holds ( b5 = eval (p,x) iff ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((BagOrder n),(Support p))) & b5 = 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)) ) ) ); theorem Th19: :: POLYNOM2:19 for n being Ordinal for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for p being Polynomial of n,L for b being bag of n st Support p = {b} holds for x being Function of n,L holds eval (p,x) = (p . b) * (eval (b,x)) proofend; theorem Th20: :: POLYNOM2:20 for n being Ordinal for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for x being Function of n,L holds eval ((0_ (n,L)),x) = 0. L proofend; theorem Th21: :: POLYNOM2:21 for n being Ordinal for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for x being Function of n,L holds eval ((1_ (n,L)),x) = 1. L proofend; theorem Th22: :: POLYNOM2:22 for n being Ordinal for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for p being Polynomial of n,L for x being Function of n,L holds eval ((- p),x) = - (eval (p,x)) proofend; Lm10: for n being Ordinal for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for p, q being Polynomial of n,L for x being Function of n,L for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds q . b9 = p . b9 ) holds eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x))) proofend; Lm11: for n being Ordinal for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for p being Polynomial of n,L st ex b being bag of n st Support p = {b} holds for q being Polynomial of n,L for x being Function of n,L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) proofend; theorem Th23: :: POLYNOM2:23 for n being Ordinal for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for p, q being Polynomial of n,L for x being Function of n,L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) proofend; theorem :: POLYNOM2:24 for n being Ordinal for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for p, q being Polynomial of n,L for x being Function of n,L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x)) proofend; Lm12: for n being Ordinal for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for p, q being Polynomial of n,L for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) proofend; Lm13: for n being Ordinal for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for q being Polynomial of n,L st ex b being bag of n st Support q = {b} holds for p being Polynomial of n,L for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) proofend; theorem Th25: :: POLYNOM2:25 for n being Ordinal for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for p, q being Polynomial of n,L for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) proofend; begin definition let n be Ordinal; let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; let x be Function of n,L; func Polynom-Evaluation (n,L,x) -> Function of (Polynom-Ring (n,L)),L means :Def5: :: POLYNOM2:def 5 for p being Polynomial of n,L holds it . p = eval (p,x); existence ex b1 being Function of (Polynom-Ring (n,L)),L st for p being Polynomial of n,L holds b1 . p = eval (p,x) proofend; uniqueness for b1, b2 being Function of (Polynom-Ring (n,L)),L st ( for p being Polynomial of n,L holds b1 . p = eval (p,x) ) & ( for p being Polynomial of n,L holds b2 . p = eval (p,x) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines Polynom-Evaluation POLYNOM2:def_5_:_ for n being Ordinal for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr for x being Function of n,L for b4 being Function of (Polynom-Ring (n,L)),L holds ( b4 = Polynom-Evaluation (n,L,x) iff for p being Polynomial of n,L holds b4 . p = eval (p,x) ); registration let n be Ordinal; let L be non empty non trivial right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; cluster Polynom-Ring (n,L) -> well-unital ; coherence Polynom-Ring (n,L) is well-unital ; end; registration let n be Ordinal; let L be non empty non trivial right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; let x be Function of n,L; cluster Polynom-Evaluation (n,L,x) -> unity-preserving ; coherence Polynom-Evaluation (n,L,x) is unity-preserving proofend; end; registration let n be Ordinal; let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; let x be Function of n,L; cluster Polynom-Evaluation (n,L,x) -> additive ; coherence Polynom-Evaluation (n,L,x) is additive proofend; end; registration let n be Ordinal; let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; let x be Function of n,L; cluster Polynom-Evaluation (n,L,x) -> multiplicative ; coherence Polynom-Evaluation (n,L,x) is multiplicative proofend; end; registration let n be Ordinal; let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; let x be Function of n,L; cluster Polynom-Evaluation (n,L,x) -> RingHomomorphism ; coherence Polynom-Evaluation (n,L,x) is RingHomomorphism proofend; end;