:: Evaluation of Multivariate Polynomials
:: by Christoph Schwarzweller and Andrzej Trybulec
::
:: Copyright (c) 2000-2018 Association of Mizar Users

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 )

proof end;

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

proof end;

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

proof end;

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 () . (a,(n + m)) = (() . (a,n)) * (() . (a,m))
proof end;

registration
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 )
proof end;
end;

theorem :: POLYNOM2:2
canceled;

::$CT theorem Th2: :: 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 proof end; 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 proof end; theorem Th4: :: 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) proof end; theorem Th5: :: 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 * () proof 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 :Def1: :: POLYNOM2:def 2 ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((),())) & it = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds y /. i = () . (((x * (SgmX ((),()))) /. i),((b * (SgmX ((),()))) /. i)) ) ); existence ex b1 being Element of L ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((),())) & b1 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds y /. i = () . (((x * (SgmX ((),()))) /. i),((b * (SgmX ((),()))) /. i)) ) ) proof end; uniqueness for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((),())) & b1 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds y /. i = () . (((x * (SgmX ((),()))) /. i),((b * (SgmX ((),()))) /. i)) ) ) & ex y being FinSequence of the carrier of L st ( len y = len (SgmX ((),())) & b2 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds y /. i = () . (((x * (SgmX ((),()))) /. i),((b * (SgmX ((),()))) /. i)) ) ) holds b1 = b2 proof end; end; :: deftheorem POLYNOM2:def 1 : canceled; :: deftheorem Def1 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 ((),())) & b5 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds y /. i = () . (((x * (SgmX ((),()))) /. i),((b * (SgmX ((),()))) /. i)) ) ) ); theorem :: POLYNOM2:7 canceled; theorem :: POLYNOM2:8 canceled; theorem :: POLYNOM2:9 canceled; theorem :: POLYNOM2:10 canceled; theorem :: POLYNOM2:11 canceled; theorem :: POLYNOM2:12 canceled; theorem :: POLYNOM2:13 canceled; ::$CT 7
theorem Th6: :: POLYNOM2:14
for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for x being Function of n,L holds eval ((),x) = 1. L
proof end;

theorem Th7: :: 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) = () . ((x . u),(b . u))
proof end;

Lm4: 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 object st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being object st u9 <> u holds
b2 . u9 = b1 . u9 ) holds
for x being Function of n,L
for a being Element of L st a = () . ((x . u),(b2 . u)) holds
eval (b2,x) = a * (eval (b1,x))

proof end;

Lm5: 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))

proof end;

theorem Th8: :: 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))
proof end;

registration
let n be Ordinal;
let p, q be Polynomial of n,L;
coherence
p - q is finite-Support
proof end;
end;

theorem Th9: :: 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)
proof end;

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 K686(L,p) -> finite ;
coherence by POLYNOM1:def 5;
end;

theorem Th10: :: 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
proof end;

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 :Def2: :: POLYNOM2:def 4
ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((),())) & it = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) ) );
existence
ex b1 being Element of L ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((),())) & b1 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) ) )
proof end;
uniqueness
for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((),())) & b1 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) ) ) & ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((),())) & b2 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem POLYNOM2:def 3 :
canceled;

:: deftheorem Def2 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 ((),())) & b5 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) ) ) );

theorem Th11: :: 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))
proof end;

theorem Th12: :: 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
proof end;

theorem Th13: :: 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
proof end;

theorem Th14: :: 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))
proof end;

Lm6: 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 = () \/ {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)))

proof end;

Lm7: 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))

proof end;

theorem Th15: :: 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))
proof end;

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

Lm8: 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))

proof end;

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 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))

proof end;

theorem Th17: :: 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))
proof end;

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 :Def3: :: 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)
proof end;
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
proof end;
end;

:: deftheorem Def3 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;
coherence
Polynom-Evaluation (n,L,x) is unity-preserving
proof end;
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
proof end;
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
proof end;
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;
coherence
Polynom-Evaluation (n,L,x) is RingHomomorphism
;
end;