:: More About Polynomials: Monomials and Constant Polynomials
:: by Christoph Schwarzweller
::
:: Received November 28, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

registration
cluster non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive domRing-like left_zeroed for doubleLoopStr ;
existence
 ex b1 being non trivial doubleLoopStr st
( b1 is Abelian & b1 is left_zeroed & b1 is right_zeroed & b1 is add-associative & b1 is right_complementable & b1 is well-unital & b1 is associative & b1 is commutative & b1 is distributive & b1 is domRing-like )
proofend;
end;

definition
let X be set ;
let R be non empty ZeroStr ;
let p be Series of X,R;
attrp is non-zero  means :Def1: :: POLYNOM7:def 1
p <> 0_ (X,R);
end;

:: deftheorem Def1 defines non-zero POLYNOM7:def_1_:_
 for X being set
for R being non empty ZeroStr
for p being Series of X,R holds
( p is non-zero iff p <> 0_ (X,R) );

registration
let X be set ;
let R be non trivial ZeroStr ;
cluster Relation-like Bags X -defined the carrier of R -valued Function-like V18( Bags X, the carrier of R) non-zero for Element of bool [:(Bags X), the carrier of R:];
existence
 ex b1 being Series of X,R st b1 is non-zero
proofend;
end;

registration
let n be Ordinal;
let R be non trivial ZeroStr ;
cluster Relation-like Bags n -defined the carrier of R -valued Function-like V18( Bags n, the carrier of R) finite-Support non-zero for Element of bool [:(Bags n), the carrier of R:];
existence
 ex b1 being Polynomial of n,R st b1 is non-zero
proofend;
end;

theorem Th1: :: POLYNOM7:1
for X being set
for R being non empty ZeroStr
for s being Series of X,R holds
( s = 0_ (X,R) iff Support s = {} )
proofend;

theorem :: POLYNOM7:2
for X being set
for R being non empty ZeroStr holds
( not R is trivial iff ex s being Series of X,R st Support s <> {} )
proofend;

definition
let X be set ;
let b be bag of X;
attrb is univariate  means :Def2: :: POLYNOM7:def 2
 ex u being Element of X st support b = {u};
end;

:: deftheorem Def2 defines univariate POLYNOM7:def_2_:_
 for X being set
for b being bag of X holds
( b is univariate iff ex u being Element of X st support b = {u} );

registration
let X be non empty set ;
cluster Relation-like X -defined Function-like total V208() finite-support univariate for set ;
existence
 ex b1 being bag of X st b1 is univariate
proofend;
end;

registration
let X be non empty set ;
cluster Relation-like X -defined Function-like total V208() finite-support univariate  ->  non empty for set ;
coherence
 for b1 being bag of X st b1 is univariate holds
not b1 is empty
proofend;
end;

begin

theorem :: POLYNOM7:3
for b being bag of {} holds b = EmptyBag {}
proofend;

Lm1:  for L being non empty doubleLoopStr
for p being Polynomial of {},L ex a being Element of L st p = {(EmptyBag {})} --> a
proofend;

theorem :: POLYNOM7:4
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of {},L
for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})
proofend;

theorem :: POLYNOM7:5
for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring ({},L) is_ringisomorph_to L
proofend;

begin

definition
let X be set ;
let L be non empty ZeroStr ;
let p be Series of X,L;
attrp is monomial-like  means :Def3: :: 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;

:: deftheorem Def3 defines monomial-like POLYNOM7:def_3_:_
 for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is monomial-like iff ex b being bag of X st
for b9 being bag of X st b9 <> b holds
p . b9 = 0. L );

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Relation-like Bags X -defined the carrier of L -valued Function-like V18( Bags X, the carrier of L) monomial-like for Element of bool [:(Bags X), the carrier of L:];
existence
 ex b1 being Series of X,L st b1 is monomial-like
proofend;
end;

definition
let X be set ;
let L be non empty ZeroStr ;
mode Monomial of X,L is monomial-like Series of X,L;
end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Function-like V18( Bags X, the carrier of L) monomial-like  ->  finite-Support for Element of bool [:(Bags X), the carrier of L:];
coherence
 for b1 being Series of X,L st b1 is monomial-like holds
b1 is finite-Support
proofend;
end;

theorem Th6: :: POLYNOM7:6
for X being set
for L being non empty ZeroStr
for 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} ) )
proofend;

definition
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
let b be bag of X;
func Monom (a,b) ->  Monomial of X,L equals :: POLYNOM7:def 4
(0_ (X,L)) +* (b,a);
coherence
 (0_ (X,L)) +* (b,a) is Monomial of X,L
proofend;
end;

:: deftheorem  defines Monom POLYNOM7:def_4_:_
 for X being set
for L being non empty ZeroStr
for a being Element of L
for b being bag of X holds Monom (a,b) = (0_ (X,L)) +* (b,a);

definition
let X be set ;
let L be non empty ZeroStr ;
let m be Monomial of X,L;
func term m ->  bag of X means :Def5: :: POLYNOM7:def 5
( m . it <> 0. L or ( Support m = {} &amp; it = EmptyBag X ) );
existence
 ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} &amp; b1 = EmptyBag X ) )
proofend;
uniqueness
 for b1, b2 being bag of X st ( m . b1 <> 0. L or ( Support m = {} &amp; b1 = EmptyBag X ) ) &amp; ( m . b2 <> 0. L or ( Support m = {} &amp; b2 = EmptyBag X ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines term POLYNOM7:def_5_:_
 for X being set
for L being non empty ZeroStr
for m being Monomial of X,L
for b4 being bag of X holds
( b4 = term m iff ( m . b4 <> 0. L or ( Support m = {} &amp; b4 = EmptyBag X ) ) );

definition
let X be set ;
let L be non empty ZeroStr ;
let m be Monomial of X,L;
func coefficient m ->  Element of L equals :: POLYNOM7:def 6
m . (term m);
coherence
 m . (term m) is Element of L ;
end;

:: deftheorem  defines coefficient POLYNOM7:def_6_:_
 for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds coefficient m = m . (term m);

theorem Th7: :: POLYNOM7:7
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds
( Support m = {} or Support m = {(term m)} )
proofend;

theorem Th8: :: POLYNOM7:8
for X being set
for L being non empty ZeroStr
for b being bag of X holds
( coefficient (Monom ((0. L),b)) = 0. L &amp; term (Monom ((0. L),b)) = EmptyBag X )
proofend;

theorem Th9: :: POLYNOM7:9
for X being set
for L being non empty ZeroStr
for a being Element of L
for b being bag of X holds coefficient (Monom (a,b)) = a
proofend;

theorem Th10: :: POLYNOM7:10
for X being set
for L being non trivial ZeroStr
for a being non zero Element of L
for b being bag of X holds term (Monom (a,b)) = b
proofend;

theorem :: POLYNOM7:11
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds Monom ((coefficient m),(term m)) = m
proofend;

theorem Th12: :: POLYNOM7:12
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for m being Monomial of n,L
for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))
proofend;

theorem :: POLYNOM7:13
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
proofend;

begin

definition
let X be set ;
let L be non empty ZeroStr ;
let p be Series of X,L;
attrp is Constant  means :Def7: :: POLYNOM7:def 7
 for b being bag of X st b <> EmptyBag X holds
p . b = 0. L;
end;

:: deftheorem Def7 defines Constant POLYNOM7:def_7_:_
 for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is Constant iff for b being bag of X st b <> EmptyBag X holds
p . b = 0. L );

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Relation-like Bags X -defined the carrier of L -valued Function-like V18( Bags X, the carrier of L) Constant for Element of bool [:(Bags X), the carrier of L:];
existence
 ex b1 being Series of X,L st b1 is Constant
proofend;
end;

definition
let X be set ;
let L be non empty ZeroStr ;
mode ConstPoly of X,L is Constant Series of X,L;
end;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster Function-like V18( Bags X, the carrier of L) Constant  ->  monomial-like for Element of bool [:(Bags X), the carrier of L:];
coherence
 for b1 being Series of X,L st b1 is Constant holds
b1 is monomial-like
proofend;
end;

theorem Th14: :: POLYNOM7:14
for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ( p = 0_ (X,L) or Support p = {(EmptyBag X)} ) )
proofend;

registration
let X be set ;
let L be non empty ZeroStr ;
cluster 0_ (X,L) ->  Constant ;
coherence
 0_ (X,L) is Constant
proofend;
end;

registration
let X be set ;
let L be non empty well-unital doubleLoopStr ;
cluster 1_ (X,L) ->  Constant ;
coherence
 1_ (X,L) is Constant
proofend;
end;

Lm2:  for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( term c = EmptyBag X &amp; coefficient c = c . (EmptyBag X) )
proofend;

theorem Th15: :: POLYNOM7:15
for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( Support c = {} or Support c = {(EmptyBag X)} )
proofend;

theorem :: POLYNOM7:16
for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( term c = EmptyBag X &amp; coefficient c = c . (EmptyBag X) ) by Lm2;

definition
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
funca | (X,L) ->  Series of X,L equals :: POLYNOM7:def 8
(0_ (X,L)) +* ((EmptyBag X),a);
coherence
 (0_ (X,L)) +* ((EmptyBag X),a) is Series of X,L ;
end;

:: deftheorem  defines | POLYNOM7:def_8_:_
 for X being set
for L being non empty ZeroStr
for a being Element of L holds a | (X,L) = (0_ (X,L)) +* ((EmptyBag X),a);

registration
let X be set ;
let L be non empty ZeroStr ;
let a be Element of L;
clustera | (X,L) ->  Constant ;
coherence
 a | (X,L) is Constant
proofend;
end;

Lm3:  for X being set
for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L)
proofend;

theorem :: POLYNOM7:17
for X being set
for L being non empty ZeroStr
for 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) )
proofend;

theorem Th18: :: POLYNOM7:18
for X being set
for L being non empty multLoopStr_0
for a being Element of L holds
( (a | (X,L)) . (EmptyBag X) = a &amp; ( for b being bag of X st b <> EmptyBag X holds
(a | (X,L)) . b = 0. L ) )
proofend;

theorem :: POLYNOM7:19
for X being set
for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L) by Lm3;

theorem :: POLYNOM7:20
for X being set
for L being non empty well-unital multLoopStr_0 holds (1. L) | (X,L) = 1_ (X,L)
proofend;

theorem :: POLYNOM7:21
for X being set
for L being non empty ZeroStr
for a, b being Element of L holds
( a | (X,L) = b | (X,L) iff a = b )
proofend;

theorem :: POLYNOM7:22
for X being set
for L being non empty ZeroStr
for a being Element of L holds
( Support (a | (X,L)) = {} or Support (a | (X,L)) = {(EmptyBag X)} ) by Th15;

theorem Th23: :: POLYNOM7:23
for X being set
for L being non empty ZeroStr
for a being Element of L holds
( term (a | (X,L)) = EmptyBag X &amp; coefficient (a | (X,L)) = a )
proofend;

theorem Th24: :: POLYNOM7:24
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for c being ConstPoly of n,L
for x being Function of n,L holds eval (c,x) = coefficient c
proofend;

theorem Th25: :: POLYNOM7:25
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for x being Function of n,L holds eval ((a | (n,L)),x) = a
proofend;

begin

definition
let X be set ;
let L be non empty multLoopStr_0 ;
let p be Series of X,L;
let a be Element of L;
funca * p ->  Series of X,L means :Def9: :: POLYNOM7:def 9
 for b being bag of X holds it . b = a * (p . b);
existence
 ex b1 being Series of X,L st
for b being bag of X holds b1 . b = a * (p . b)
proofend;
uniqueness
 for b1, b2 being Series of X,L st ( for b being bag of X holds b1 . b = a * (p . b) ) &amp; ( for b being bag of X holds b2 . b = a * (p . b) ) holds
b1 = b2
proofend;
funcp * a ->  Series of X,L means :Def10: :: POLYNOM7:def 10
 for b being bag of X holds it . b = (p . b) * a;
existence
 ex b1 being Series of X,L st
for b being bag of X holds b1 . b = (p . b) * a
proofend;
uniqueness
 for b1, b2 being Series of X,L st ( for b being bag of X holds b1 . b = (p . b) * a ) &amp; ( for b being bag of X holds b2 . b = (p . b) * a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines * POLYNOM7:def_9_:_
 for X being set
for L being non empty multLoopStr_0
for p being Series of X,L
for a being Element of L
for b5 being Series of X,L holds
( b5 = a * p iff for b being bag of X holds b5 . b = a * (p . b) );

:: deftheorem Def10 defines * POLYNOM7:def_10_:_
 for X being set
for L being non empty multLoopStr_0
for p being Series of X,L
for a being Element of L
for b5 being Series of X,L holds
( b5 = p * a iff for b being bag of X holds b5 . b = (p . b) * a );

registration
let X be set ;
let L be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ;
let p be finite-Support Series of X,L;
let a be Element of L;
clustera * p ->  finite-Support ;
coherence
 a * p is finite-Support
proofend;
clusterp * a ->  finite-Support ;
coherence
 p * a is finite-Support
proofend;
end;

theorem :: POLYNOM7:26
for X being set
for L being non empty commutative multLoopStr_0
for p being Series of X,L
for a being Element of L holds a * p = p * a
proofend;

theorem Th27: :: POLYNOM7:27
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds a * p = (a | (n,L)) *' p
proofend;

theorem Th28: :: POLYNOM7:28
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds p * a = p *' (a | (n,L))
proofend;

Lm4:  for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
proofend;

Lm5:  for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
proofend;

theorem :: POLYNOM7:29
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
proofend;

theorem :: POLYNOM7:30
for n being Ordinal
for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative well-unital distributive domRing-like left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((a * p),x) = a * (eval (p,x))
proofend;

theorem :: POLYNOM7:31
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
proofend;

theorem :: POLYNOM7:32
for n being Ordinal
for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative commutative well-unital distributive domRing-like left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a
proofend;

theorem :: POLYNOM7:33
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x)) by Lm4;

theorem :: POLYNOM7:34
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
proofend;