:: by Christoph Schwarzweller

::

:: Received November 28, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

registration

ex b_{1} being non trivial doubleLoopStr st

( b_{1} is Abelian & b_{1} is left_zeroed & b_{1} is right_zeroed & b_{1} is add-associative & b_{1} is right_complementable & b_{1} is well-unital & b_{1} is associative & b_{1} is commutative & b_{1} is distributive & b_{1} is domRing-like )
end;

cluster non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative domRing-like left_zeroed for doubleLoopStr ;

existence ex b

( b

proof end;

:: deftheorem 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) );

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 ;

ex b_{1} being Series of X,R st b_{1} is non-zero

end;
let R be non trivial ZeroStr ;

cluster Relation-like Bags X -defined the carrier of R -valued Function-like quasi_total non-zero for Element of bool [:(Bags X), the carrier of R:];

existence ex b

proof end;

registration

let n be Ordinal;

let R be non trivial ZeroStr ;

ex b_{1} being Polynomial of n,R st b_{1} is non-zero

end;
let R be non trivial ZeroStr ;

cluster Relation-like Bags n -defined the carrier of R -valued Function-like quasi_total finite-Support non-zero for Element of bool [:(Bags n), the carrier of R:];

existence ex b

proof 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 = {} )

for R being non empty ZeroStr

for s being Series of X,R holds

( s = 0_ (X,R) iff Support s = {} )

proof end;

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

for R being non empty ZeroStr holds

( not R is trivial iff ex s being Series of X,R st Support s <> {} )

proof end;

:: deftheorem 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} );

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

registration

let X be non empty set ;

for b_{1} being bag of X st b_{1} is univariate holds

not b_{1} is V3()

end;
cluster Relation-like X -defined Function-like total V204() finite-support univariate -> V3() for set ;

coherence for b

not b

proof end;

Lm1: for L being non empty doubleLoopStr

for p being Polynomial of {},L ex a being Element of L st p = {(EmptyBag {})} --> a

proof end;

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

for p being Polynomial of {},L

for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})

proof end;

theorem :: POLYNOM7:5

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

proof end;

definition

let X be set ;

let L be non empty ZeroStr ;

let p be Series of X,L;

end;
let L be non empty ZeroStr ;

let p be Series of X,L;

attr p 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;

ex b being bag of X st

for b9 being bag of X st b9 <> b holds

p . b9 = 0. L;

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

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 ;

ex b_{1} being Series of X,L st b_{1} is monomial-like

end;
let L be non empty ZeroStr ;

cluster Relation-like Bags X -defined the carrier of L -valued Function-like quasi_total monomial-like for Element of bool [:(Bags X), the carrier of L:];

existence ex b

proof end;

definition
end;

registration

let X be set ;

let L be non empty ZeroStr ;

for b_{1} being Series of X,L st b_{1} is monomial-like holds

b_{1} is finite-Support

end;
let L be non empty ZeroStr ;

cluster Function-like quasi_total monomial-like -> finite-Support for Element of bool [:(Bags X), the carrier of L:];

coherence for b

b

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

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

proof end;

definition

let X be set ;

let L be non empty ZeroStr ;

let a be Element of L;

let b be bag of X;

coherence

(0_ (X,L)) +* (b,a) is Monomial of X,L

end;
let L be non empty ZeroStr ;

let a be Element of L;

let b be bag of X;

coherence

(0_ (X,L)) +* (b,a) is Monomial of X,L

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

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;

ex b_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) )

for b_{1}, b_{2} being bag of X st ( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) ) & ( m . b_{2} <> 0. L or ( Support m = {} & b_{2} = EmptyBag X ) ) holds

b_{1} = b_{2}

end;
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 = {} & it = EmptyBag X ) );

existence ( m . it <> 0. L or ( Support m = {} & it = EmptyBag X ) );

ex b

( m . b

proof end;

uniqueness for b

b

proof 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 b_{4} being bag of X holds

( b_{4} = term m iff ( m . b_{4} <> 0. L or ( Support m = {} & b_{4} = EmptyBag X ) ) );

for X being set

for L being non empty ZeroStr

for m being Monomial of X,L

for b

( b

definition

let X be set ;

let L be non empty ZeroStr ;

let m be Monomial of X,L;

coherence

m . (term m) is Element of L ;

end;
let L be non empty ZeroStr ;

let m be Monomial of X,L;

coherence

m . (term m) is Element of L ;

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

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

for L being non empty ZeroStr

for m being Monomial of X,L holds

( Support m = {} or Support m = {(term m)} )

proof end;

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 & term (Monom ((0. L),b)) = EmptyBag X )

for L being non empty ZeroStr

for b being bag of X holds

( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag X )

proof end;

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

for L being non empty ZeroStr

for a being Element of L

for b being bag of X holds coefficient (Monom (a,b)) = a

proof end;

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

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

proof end;

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

for L being non empty ZeroStr

for m being Monomial of X,L holds Monom ((coefficient m),(term m)) = m

proof end;

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

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

proof end;

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

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

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

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 ;

ex b_{1} being Series of X,L st b_{1} is Constant

end;
let L be non empty ZeroStr ;

cluster Relation-like Bags X -defined the carrier of L -valued Function-like quasi_total Constant for Element of bool [:(Bags X), the carrier of L:];

existence ex b

proof end;

definition
end;

registration

let X be set ;

let L be non empty ZeroStr ;

for b_{1} being Series of X,L st b_{1} is Constant holds

b_{1} is monomial-like
;

end;
let L be non empty ZeroStr ;

cluster Function-like quasi_total Constant -> monomial-like for Element of bool [:(Bags X), the carrier of L:];

coherence for b

b

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

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

proof end;

registration
end;

registration

let X be set ;

let L be non empty well-unital doubleLoopStr ;

coherence

1_ (X,L) is Constant by POLYNOM1:25;

end;
let L be non empty well-unital doubleLoopStr ;

coherence

1_ (X,L) is Constant by POLYNOM1:25;

Lm2: for X being set

for L being non empty ZeroStr

for c being ConstPoly of X,L holds

( term c = EmptyBag X & coefficient c = c . (EmptyBag X) )

proof end;

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

for L being non empty ZeroStr

for c being ConstPoly of X,L holds

( Support c = {} or Support c = {(EmptyBag X)} )

proof end;

theorem :: POLYNOM7:16

definition

let X be set ;

let L be non empty ZeroStr ;

let a be Element of L;

coherence

(0_ (X,L)) +* ((EmptyBag X),a) is Series of X,L ;

end;
let L be non empty ZeroStr ;

let a be Element of L;

coherence

(0_ (X,L)) +* ((EmptyBag X),a) is Series of X,L ;

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

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;

coherence

a | (X,L) is Constant

end;
let L be non empty ZeroStr ;

let a be Element of L;

coherence

a | (X,L) is Constant

proof end;

Lm3: for X being set

for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L)

proof end;

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

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

proof end;

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 & ( for b being bag of X st b <> EmptyBag X holds

(a | (X,L)) . b = 0. L ) )

for L being non empty multLoopStr_0

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

proof end;

theorem :: POLYNOM7:19

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 )

for L being non empty ZeroStr

for a, b being Element of L holds

( a | (X,L) = b | (X,L) iff a = b )

proof end;

theorem :: POLYNOM7:22

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 & coefficient (a | (X,L)) = a )

for L being non empty ZeroStr

for a being Element of L holds

( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )

proof end;

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

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

proof end;

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

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

proof end;

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;

ex b_{1} being Series of X,L st

for b being bag of X holds b_{1} . b = a * (p . b)

for b_{1}, b_{2} being Series of X,L st ( for b being bag of X holds b_{1} . b = a * (p . b) ) & ( for b being bag of X holds b_{2} . b = a * (p . b) ) holds

b_{1} = b_{2}

ex b_{1} being Series of X,L st

for b being bag of X holds b_{1} . b = (p . b) * a

for b_{1}, b_{2} being Series of X,L st ( for b being bag of X holds b_{1} . b = (p . b) * a ) & ( for b being bag of X holds b_{2} . b = (p . b) * a ) holds

b_{1} = b_{2}

end;
let L be non empty multLoopStr_0 ;

let p be Series of X,L;

let a be Element of L;

func a * p -> Series of X,L means :Def9: :: POLYNOM7:def 9

for b being bag of X holds it . b = a * (p . b);

existence for b being bag of X holds it . b = a * (p . b);

ex b

for b being bag of X holds b

proof end;

uniqueness for b

b

proof end;

func p * a -> Series of X,L means :Def10: :: POLYNOM7:def 10

for b being bag of X holds it . b = (p . b) * a;

existence for b being bag of X holds it . b = (p . b) * a;

ex b

for b being bag of X holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being Series of X,L holds

( b_{5} = a * p iff for b being bag of X holds b_{5} . b = a * (p . b) );

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 b

( 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 b_{5} being Series of X,L holds

( b_{5} = p * a iff for b being bag of X holds b_{5} . b = (p . b) * a );

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 b

( b

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;

coherence

a * p is finite-Support

p * a is finite-Support

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

coherence

a * p is finite-Support

proof end;

coherence p * a is finite-Support

proof 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

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

proof end;

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

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

proof end;

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

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

proof end;

Lm4: for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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))

proof end;

Lm5: for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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

proof end;

theorem :: POLYNOM7:29

for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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))

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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))

proof end;

theorem :: POLYNOM7:30

for n being Ordinal

for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed well-unital distributive associative 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))

for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed well-unital distributive associative 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))

proof end;

theorem :: POLYNOM7:31

for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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

proof end;

theorem :: POLYNOM7:32

for n being Ordinal

for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed well-unital distributive associative commutative 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

for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed well-unital distributive associative commutative 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

proof end;

theorem :: POLYNOM7:33

for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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;

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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 well-unital distributive associative commutative 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

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative 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

proof end;