:: by Piotr Rudnicki and Andrzej Trybulec

::

:: Received September 22, 1999

:: Copyright (c) 1999-2017 Association of Mizar Users

registration

for b_{1} being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st b_{1} is degenerated holds

b_{1} is trivial
end;

cluster non empty degenerated right_complementable right-distributive right_unital add-associative right_zeroed -> non empty trivial right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;

coherence for b

b

proof end;

registration

for b_{1} being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st not b_{1} is trivial holds

not b_{1} is degenerated
;

end;

cluster non empty non trivial right_complementable right-distributive right_unital add-associative right_zeroed -> non empty non degenerated right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;

coherence for b

not b

theorem Th1: :: POLYNOM1:1

for K being non empty addLoopStr

for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds

dom (p1 + p2) = dom p1

for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds

dom (p1 + p2) = dom p1

proof end;

theorem Th2: :: POLYNOM1:2

for L being non empty addLoopStr

for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F

for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F

proof end;

theorem Th3: :: POLYNOM1:3

for L being non empty addLoopStr

for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L

for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L

proof end;

theorem Th4: :: POLYNOM1:4

for L being non empty addLoopStr

for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>

for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>

proof end;

theorem Th5: :: POLYNOM1:5

for L being non empty addLoopStr

for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)

for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)

proof end;

definition

let L be non empty multMagma ;

let p be FinSequence of the carrier of L;

let a be Element of L;

for b_{1} being FinSequence of the carrier of L holds

( b_{1} = a * p iff ( dom b_{1} = dom p & ( for i being object st i in dom p holds

b_{1} /. i = a * (p /. i) ) ) )

end;
let p be FinSequence of the carrier of L;

let a be Element of L;

redefine func a * p means :Def1: :: POLYNOM1:def 1

( dom it = dom p & ( for i being object st i in dom p holds

it /. i = a * (p /. i) ) );

compatibility ( dom it = dom p & ( for i being object st i in dom p holds

it /. i = a * (p /. i) ) );

for b

( b

b

proof end;

:: deftheorem Def1 defines * POLYNOM1:def 1 :

for L being non empty multMagma

for p being FinSequence of the carrier of L

for a being Element of L

for b_{4} being FinSequence of the carrier of L holds

( b_{4} = a * p iff ( dom b_{4} = dom p & ( for i being object st i in dom p holds

b_{4} /. i = a * (p /. i) ) ) );

for L being non empty multMagma

for p being FinSequence of the carrier of L

for a being Element of L

for b

( b

b

definition

let L be non empty multMagma ;

let p be FinSequence of the carrier of L;

let a be Element of L;

ex b_{1} being FinSequence of the carrier of L st

( dom b_{1} = dom p & ( for i being object st i in dom p holds

b_{1} /. i = (p /. i) * a ) )

for b_{1}, b_{2} being FinSequence of the carrier of L st dom b_{1} = dom p & ( for i being object st i in dom p holds

b_{1} /. i = (p /. i) * a ) & dom b_{2} = dom p & ( for i being object st i in dom p holds

b_{2} /. i = (p /. i) * a ) holds

b_{1} = b_{2}

end;
let p be FinSequence of the carrier of L;

let a be Element of L;

func p * a -> FinSequence of the carrier of L means :Def2: :: POLYNOM1:def 2

( dom it = dom p & ( for i being object st i in dom p holds

it /. i = (p /. i) * a ) );

existence ( dom it = dom p & ( for i being object st i in dom p holds

it /. i = (p /. i) * a ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines * POLYNOM1:def 2 :

for L being non empty multMagma

for p being FinSequence of the carrier of L

for a being Element of L

for b_{4} being FinSequence of the carrier of L holds

( b_{4} = p * a iff ( dom b_{4} = dom p & ( for i being object st i in dom p holds

b_{4} /. i = (p /. i) * a ) ) );

for L being non empty multMagma

for p being FinSequence of the carrier of L

for a being Element of L

for b

( b

b

theorem Th6: :: POLYNOM1:6

for L being non empty multMagma

for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L

for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L

proof end;

theorem Th7: :: POLYNOM1:7

for L being non empty multMagma

for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L

for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L

proof end;

theorem Th10: :: POLYNOM1:10

for L being non empty multMagma

for a being Element of L

for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q)

for a being Element of L

for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q)

proof end;

theorem Th11: :: POLYNOM1:11

for L being non empty multMagma

for a being Element of L

for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)

for a being Element of L

for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)

proof end;

registration
end;

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is associative & b_{1} is commutative & b_{1} is distributive & b_{1} is almost_left_invertible & b_{1} is well-unital & not b_{1} is trivial )
end;

cluster non empty non trivial right_complementable almost_left_invertible strict well-unital distributive Abelian add-associative right_zeroed associative commutative for doubleLoopStr ;

existence ex b

( b

proof end;

theorem Th12: :: POLYNOM1:12

for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for a being Element of L

for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)

for a being Element of L

for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)

proof end;

theorem Th13: :: POLYNOM1:13

for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for a being Element of L

for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a

for a being Element of L

for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a

proof end;

theorem Th14: :: POLYNOM1:14

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F)

for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F)

proof end;

definition

let S be ZeroStr ;

let f be the carrier of S -valued Function;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ( x in dom f & f . x <> 0. S ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ( x in dom f & f . x <> 0. S ) ) ) & ( for x being object holds

( x in b_{2} iff ( x in dom f & f . x <> 0. S ) ) ) holds

b_{1} = b_{2}

end;
let f be the carrier of S -valued Function;

func Support f -> set means :Def3: :: POLYNOM1:def 3

for x being object holds

( x in it iff ( x in dom f & f . x <> 0. S ) );

existence for x being object holds

( x in it iff ( x in dom f & f . x <> 0. S ) );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines Support POLYNOM1:def 3 :

for S being ZeroStr

for f being the carrier of b_{1} -valued Function

for b_{3} being set holds

( b_{3} = Support f iff for x being object holds

( x in b_{3} iff ( x in dom f & f . x <> 0. S ) ) );

for S being ZeroStr

for f being the carrier of b

for b

( b

( x in b

definition

let X be non empty set ;

let S be non empty ZeroStr ;

let f be Function of X,S;

Support f is Subset of X

for b_{1} being Subset of X holds

( b_{1} = Support f iff for x being Element of X holds

( x in b_{1} iff f . x <> 0. S ) )

end;
let S be non empty ZeroStr ;

let f be Function of X,S;

:: original: Support

redefine func Support f -> Subset of X means :Def4: :: POLYNOM1:def 4

for x being Element of X holds

( x in it iff f . x <> 0. S );

coherence redefine func Support f -> Subset of X means :Def4: :: POLYNOM1:def 4

for x being Element of X holds

( x in it iff f . x <> 0. S );

Support f is Subset of X

proof end;

compatibility for b

( b

( x in b

proof end;

:: deftheorem Def4 defines Support POLYNOM1:def 4 :

for X being non empty set

for S being non empty ZeroStr

for f being Function of X,S

for b_{4} being Subset of X holds

( b_{4} = Support f iff for x being Element of X holds

( x in b_{4} iff f . x <> 0. S ) );

for X being non empty set

for S being non empty ZeroStr

for f being Function of X,S

for b

( b

( x in b

:: deftheorem Def5 defines finite-Support POLYNOM1:def 5 :

for S being ZeroStr

for p being the carrier of b_{1} -valued Function holds

( p is finite-Support iff Support p is finite );

for S being ZeroStr

for p being the carrier of b

( p is finite-Support iff Support p is finite );

definition

let n be set ;

let L be non empty 1-sorted ;

let p be Function of (Bags n),L;

let x be bag of n;

:: original: .

redefine func p . x -> Element of L;

coherence

p . x is Element of L

end;
let L be non empty 1-sorted ;

let p be Function of (Bags n),L;

let x be bag of n;

:: original: .

redefine func p . x -> Element of L;

coherence

p . x is Element of L

proof end;

definition

let n be set ;

let L be non empty addLoopStr ;

let p, q be Series of n,L;

coherence

p + q is Series of n,L ;

end;
let L be non empty addLoopStr ;

let p, q be Series of n,L;

coherence

p + q is Series of n,L ;

:: deftheorem defines + POLYNOM1:def 6 :

for n being set

for L being non empty addLoopStr

for p, q being Series of n,L holds p + q = p + q;

for n being set

for L being non empty addLoopStr

for p, q being Series of n,L holds p + q = p + q;

theorem Th15: :: POLYNOM1:15

for n being set

for L being non empty addLoopStr

for p, q being Series of n,L

for x being bag of n holds (p + q) . x = (p . x) + (q . x)

for L being non empty addLoopStr

for p, q being Series of n,L

for x being bag of n holds (p + q) . x = (p . x) + (q . x)

proof end;

theorem :: POLYNOM1:16

for n being set

for L being non empty addLoopStr

for 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

for L being non empty addLoopStr

for 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

proof end;

theorem Th17: :: POLYNOM1:17

for n being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L

for x being bag of n holds (- p) . x = - (p . x)

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L

for x being bag of n holds (- p) . x = - (p . x)

proof end;

theorem :: POLYNOM1:18

for n being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds

r = - p

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds

r = - p

proof end;

theorem :: POLYNOM1:19

for n being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L holds p = - (- p)

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L holds p = - (- p)

proof end;

theorem Th20: :: POLYNOM1:20

for n being set

for L being non empty right_zeroed addLoopStr

for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)

for L being non empty right_zeroed addLoopStr

for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)

proof end;

definition

let n be set ;

let L be non empty Abelian right_zeroed addLoopStr ;

let p, q be Series of n,L;

:: original: +

redefine func p + q -> Series of n,L;

commutativity

for p, q being Series of n,L holds p + q = q + p

end;
let L be non empty Abelian right_zeroed addLoopStr ;

let p, q be Series of n,L;

:: original: +

redefine func p + q -> Series of n,L;

commutativity

for p, q being Series of n,L holds p + q = q + p

proof end;

theorem Th21: :: POLYNOM1:21

for n being set

for L being non empty add-associative right_zeroed doubleLoopStr

for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)

for L being non empty add-associative right_zeroed doubleLoopStr

for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)

proof end;

definition

let n be set ;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p, q be Series of n,L;

coherence

p + (- q) is Series of n,L ;

end;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p, q be Series of n,L;

coherence

p + (- q) is Series of n,L ;

:: deftheorem defines - POLYNOM1:def 7 :

for n being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p, q being Series of n,L holds p - q = p + (- q);

for n being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p, q being Series of n,L holds p - q = p + (- q);

definition
end;

:: deftheorem defines 0_ POLYNOM1:def 8 :

for n being set

for S being non empty ZeroStr holds 0_ (n,S) = (Bags n) --> (0. S);

for n being set

for S being non empty ZeroStr holds 0_ (n,S) = (Bags n) --> (0. S);

theorem Th23: :: POLYNOM1:23

for n being set

for L being non empty right_zeroed addLoopStr

for p being Series of n,L holds p + (0_ (n,L)) = p

for L being non empty right_zeroed addLoopStr

for p being Series of n,L holds p + (0_ (n,L)) = p

proof end;

definition

let n be set ;

let L be non empty right_unital multLoopStr_0 ;

coherence

(0_ (n,L)) +* ((EmptyBag n),(1. L)) is Series of n,L ;

end;
let L be non empty right_unital multLoopStr_0 ;

coherence

(0_ (n,L)) +* ((EmptyBag n),(1. L)) is Series of n,L ;

:: deftheorem defines 1_ POLYNOM1:def 9 :

for n being set

for L being non empty right_unital multLoopStr_0 holds 1_ (n,L) = (0_ (n,L)) +* ((EmptyBag n),(1. L));

for n being set

for L being non empty right_unital multLoopStr_0 holds 1_ (n,L) = (0_ (n,L)) +* ((EmptyBag n),(1. L));

theorem Th24: :: POLYNOM1:24

for n being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L holds p - p = 0_ (n,L)

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L holds p - p = 0_ (n,L)

proof end;

theorem Th25: :: POLYNOM1:25

for n being set

for L being non empty right_unital 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 ) )

for L being non empty right_unital 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 ) )

proof end;

definition

let n be Ordinal;

let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let p, q be Series of n,L;

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

for b being bag of n ex s being FinSequence of the carrier of L st

( b_{1} . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )

for b_{1}, b_{2} being Series of n,L st ( for b being bag of n ex s being FinSequence of the carrier of L st

( b_{1} . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st

( b_{2} . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) holds

b_{1} = b_{2}

end;
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let p, q be Series of n,L;

func p *' q -> Series of n,L means :Def10: :: 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 holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) );

existence 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 holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) );

ex b

for b being bag of n ex s being FinSequence of the carrier of L st

( b

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )

proof end;

uniqueness for b

( b

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st

( b

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) holds

b

proof end;

:: deftheorem Def10 defines *' POLYNOM1:def 10 :

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed doubleLoopStr

for p, q, b_{5} being Series of n,L holds

( b_{5} = p *' q iff for b being bag of n ex s being FinSequence of the carrier of L st

( b_{5} . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) );

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed doubleLoopStr

for p, q, b

( b

( b

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) );

theorem Th26: :: POLYNOM1:26

for n being Ordinal

for L being non empty right_complementable distributive Abelian add-associative right_zeroed associative doubleLoopStr

for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)

for L being non empty right_complementable distributive Abelian add-associative right_zeroed associative doubleLoopStr

for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)

proof end;

theorem Th27: :: POLYNOM1:27

for n being Ordinal

for L being non empty right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)

for L being non empty right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)

proof end;

definition

let n be Ordinal;

let L be non empty right_complementable Abelian add-associative right_zeroed commutative doubleLoopStr ;

let p, q be Series of n,L;

:: original: *'

redefine func p *' q -> Series of n,L;

commutativity

for p, q being Series of n,L holds p *' q = q *' p

end;
let L be non empty right_complementable Abelian add-associative right_zeroed commutative doubleLoopStr ;

let p, q be Series of n,L;

:: original: *'

redefine func p *' q -> Series of n,L;

commutativity

for p, q being Series of n,L holds p *' q = q *' p

proof end;

theorem :: POLYNOM1:28

for n being Ordinal

for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L)

for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L)

proof end;

theorem Th29: :: POLYNOM1:29

for n being Ordinal

for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for p being Series of n,L holds p *' (1_ (n,L)) = p

for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for p being Series of n,L holds p *' (1_ (n,L)) = p

proof end;

theorem Th30: :: POLYNOM1:30

for n being Ordinal

for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for p being Series of n,L holds (1_ (n,L)) *' p = p

for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for p being Series of n,L holds (1_ (n,L)) *' p = p

proof end;

registration

let n be set ;

let S be non empty ZeroStr ;

ex b_{1} being Series of n,S st b_{1} is finite-Support

end;
let S be non empty ZeroStr ;

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

existence ex b

proof end;

definition

let n be Ordinal;

let S be non empty ZeroStr ;

mode Polynomial of n,S is finite-Support Series of n,S;

end;
let S be non empty ZeroStr ;

mode Polynomial of n,S is finite-Support Series of n,S;

registration

let n be Ordinal;

let L be non empty right_zeroed addLoopStr ;

let p, q be Polynomial of n,L;

coherence

p + q is finite-Support

end;
let L be non empty right_zeroed addLoopStr ;

let p, q be Polynomial of n,L;

coherence

p + q is finite-Support

proof end;

registration

let n be Ordinal;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

coherence

- p is finite-Support

end;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

coherence

- p is finite-Support

proof end;

registration

let n be Element of NAT ;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p, q be Polynomial of n,L;

coherence

p - q is finite-Support ;

end;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p, q be Polynomial of n,L;

coherence

p - q is finite-Support ;

registration
end;

registration

let n be Ordinal;

let L be non trivial right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ;

coherence

1_ (n,L) is finite-Support

end;
let L be non trivial right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ;

coherence

1_ (n,L) is finite-Support

proof end;

registration

let n be Ordinal;

let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

let p, q be Polynomial of n,L;

coherence

p *' q is finite-Support

end;
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

let p, q be Polynomial of n,L;

coherence

p *' q is finite-Support

proof end;

definition

let n be Ordinal;

let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

ex b_{1} being non empty strict doubleLoopStr st

( ( for x being set holds

( x in the carrier of b_{1} iff x is Polynomial of n,L ) ) & ( for x, y being Element of b_{1}

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{1}

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b_{1} = 0_ (n,L) & 1. b_{1} = 1_ (n,L) )

for b_{1}, b_{2} being non empty strict doubleLoopStr st ( for x being set holds

( x in the carrier of b_{1} iff x is Polynomial of n,L ) ) & ( for x, y being Element of b_{1}

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{1}

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b_{1} = 0_ (n,L) & 1. b_{1} = 1_ (n,L) & ( for x being set holds

( x in the carrier of b_{2} iff x is Polynomial of n,L ) ) & ( for x, y being Element of b_{2}

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{2}

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b_{2} = 0_ (n,L) & 1. b_{2} = 1_ (n,L) holds

b_{1} = b_{2}

end;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

func Polynom-Ring (n,L) -> non empty strict doubleLoopStr means :Def11: :: 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

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of it

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

existence ( ( 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

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of it

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

ex b

( ( for x being set holds

( x in the carrier of b

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b

proof end;

uniqueness for b

( x in the carrier of b

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b

( x in the carrier of b

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b

b

proof end;

:: deftheorem Def11 defines Polynom-Ring POLYNOM1:def 11 :

for n being Ordinal

for L being non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for b_{3} being non empty strict doubleLoopStr holds

( b_{3} = Polynom-Ring (n,L) iff ( ( for x being set holds

( x in the carrier of b_{3} iff x is Polynomial of n,L ) ) & ( for x, y being Element of b_{3}

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{3}

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b_{3} = 0_ (n,L) & 1. b_{3} = 1_ (n,L) ) );

for n being Ordinal

for L being non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr

for b

( b

( x in the carrier of b

for p, q being Polynomial of n,L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being Polynomial of n,L st x = p & y = q holds

x * y = p *' q ) & 0. b

registration

let n be Ordinal;

let L be non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is Abelian

end;
let L be non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is Abelian

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is add-associative

end;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is add-associative

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is right_zeroed

end;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is right_zeroed

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is right_complementable

end;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring (n,L) is right_complementable

proof end;

registration

let n be Ordinal;

let L be non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr ;

coherence

Polynom-Ring (n,L) is commutative

end;
let L be non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr ;

coherence

Polynom-Ring (n,L) is commutative

proof end;

registration

let n be Ordinal;

let L be non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

coherence

Polynom-Ring (n,L) is associative

end;
let L be non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

coherence

Polynom-Ring (n,L) is associative

proof end;

Lm1: now :: thesis: for n being Ordinal

for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds

( x * e = x & e * x = x )

for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds

( x * e = x & e * x = x )

let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds

( x * e = x & e * x = x )

let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds

( x * e = x & e * x = x )

set Pm = Polynom-Ring (n,L);

let x, e be Element of (Polynom-Ring (n,L)); :: thesis: ( e = 1. (Polynom-Ring (n,L)) implies ( x * e = x & e * x = x ) )

reconsider p = x as Polynomial of n,L by Def11;

assume A1: e = 1. (Polynom-Ring (n,L)) ; :: thesis: ( x * e = x & e * x = x )

A2: 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def11;

hence x * e = p *' (1_ (n,L)) by A1, Def11

.= x by Th29 ;

:: thesis: e * x = x

thus e * x = (1_ (n,L)) *' p by A1, A2, Def11

.= x by Th30 ; :: thesis: verum

end;
for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds

( x * e = x & e * x = x )

let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds

( x * e = x & e * x = x )

set Pm = Polynom-Ring (n,L);

let x, e be Element of (Polynom-Ring (n,L)); :: thesis: ( e = 1. (Polynom-Ring (n,L)) implies ( x * e = x & e * x = x ) )

reconsider p = x as Polynomial of n,L by Def11;

assume A1: e = 1. (Polynom-Ring (n,L)) ; :: thesis: ( x * e = x & e * x = x )

A2: 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def11;

hence x * e = p *' (1_ (n,L)) by A1, Def11

.= x by Th29 ;

:: thesis: e * x = x

thus e * x = (1_ (n,L)) *' p by A1, A2, Def11

.= x by Th30 ; :: thesis: verum

registration

let n be Ordinal;

let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

coherence

( Polynom-Ring (n,L) is well-unital & Polynom-Ring (n,L) is right-distributive )

end;
let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

coherence

( Polynom-Ring (n,L) is well-unital & Polynom-Ring (n,L) is right-distributive )

proof end;

theorem :: POLYNOM1:31

for n being Ordinal

for L being non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr holds 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def11;

for L being non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr holds 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def11;