:: by Christoph Schwarzweller

::

:: Received December 20, 2002

:: Copyright (c) 2002-2018 Association of Mizar Users

registration

let n be Ordinal;

let R be non trivial ZeroStr ;

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

end;
let R be non trivial ZeroStr ;

cluster non empty Relation-like Bags n -defined the carrier of R -valued Function-like total V49( Bags n, the carrier of R) non-zero monomial-like finite-Support for Monomial of ,;

existence ex b

proof end;

registration

not for b_{1} being Field holds b_{1} is trivial
end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like for Field;

existence not for b

proof end;

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

Lm2: for n being Ordinal

for b1, b2, b3 being bag of n st b1 <=' b2 holds

b1 + b3 <=' b2 + b3

proof end;

Lm3: for n being Ordinal

for b1, b2 being bag of n st b1 <=' b2 & b2 <=' b1 holds

b1 = b2

proof end;

Lm4: for n being Ordinal

for b1, b2 being bag of n holds

( not b1 < b2 iff b2 <=' b1 )

proof end;

Lm5: for n being Ordinal

for L being non trivial ZeroStr

for p being non-zero finite-Support Series of n,L ex b being bag of n st

( p . b <> 0. L & ( for b9 being bag of n st b < b9 holds

p . b9 = 0. L ) )

proof end;

Lm6: for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for f, g being FinSequence of the carrier of L

for n being Nat st len f = n + 1 & g = f | (Seg n) holds

Sum f = (Sum g) + (f /. (len f))

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ;

let p, q be non-zero finite-Support Series of n,L;

coherence

p *' q is non-zero

end;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ;

let p, q be non-zero finite-Support Series of n,L;

coherence

p *' q is non-zero

proof end;

theorem Th1: :: POLYRED:1

for X being set

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

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

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

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

proof end;

theorem Th2: :: POLYRED:2

for X being set

for L being non empty left_zeroed addLoopStr

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

for L being non empty left_zeroed addLoopStr

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

proof end;

theorem Th3: :: POLYRED:3

for X being set

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of X,L holds

( (- p) + p = 0_ (X,L) & p + (- p) = 0_ (X,L) )

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of X,L holds

( (- p) + p = 0_ (X,L) & p + (- p) = 0_ (X,L) )

proof end;

theorem Th4: :: POLYRED:4

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 - (0_ (n,L)) = p

for L being non empty right_complementable add-associative right_zeroed addLoopStr

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

proof end;

theorem Th5: :: POLYRED:5

for n being Ordinal

for L being non empty left_add-cancelable right_complementable left-distributive add-associative right_zeroed doubleLoopStr

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

for L being non empty left_add-cancelable right_complementable left-distributive add-associative right_zeroed doubleLoopStr

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

proof end;

Lm7: for n being Ordinal

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

for p being Polynomial of n,L

for q being Element of (Polynom-Ring (n,L)) st p = q holds

- p = - q

proof end;

theorem Th6: :: POLYRED:6

for n being Ordinal

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

for p, q being Polynomial of n,L holds

( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )

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

for p, q being Polynomial of n,L holds

( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )

proof end;

Lm8: for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for m being Monomial of n,L

for b being bag of n st b <> term m holds

m . b = 0. L

proof end;

theorem Th7: :: POLYRED:7

for n being Ordinal

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

for p being Polynomial of n,L

for m being Monomial of n,L

for b being bag of n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)

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

for p being Polynomial of n,L

for m being Monomial of n,L

for b being bag of n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)

proof end;

theorem Th8: :: POLYRED:8

for X being set

for L being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr

for p being Series of X,L holds (0. L) * p = 0_ (X,L)

for L being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr

for p being Series of X,L holds (0. L) * p = 0_ (X,L)

proof end;

theorem Th9: :: POLYRED:9

for X being set

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

for p being Series of X,L

for a being Element of L holds

( - (a * p) = (- a) * p & - (a * p) = a * (- p) )

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

for p being Series of X,L

for a being Element of L holds

( - (a * p) = (- a) * p & - (a * p) = a * (- p) )

proof end;

theorem Th10: :: POLYRED:10

for X being set

for L being non empty left-distributive doubleLoopStr

for p being Series of X,L

for a, a9 being Element of L holds (a * p) + (a9 * p) = (a + a9) * p

for L being non empty left-distributive doubleLoopStr

for p being Series of X,L

for a, a9 being Element of L holds (a * p) + (a9 * p) = (a + a9) * p

proof end;

theorem Th11: :: POLYRED:11

for X being set

for L being non empty associative multLoopStr_0

for p being Series of X,L

for a, a9 being Element of L holds (a * a9) * p = a * (a9 * p)

for L being non empty associative multLoopStr_0

for p being Series of X,L

for a, a9 being Element of L holds (a * a9) * p = a * (a9 * p)

proof end;

theorem Th12: :: POLYRED:12

for n being Ordinal

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

for p, p9 being Series of n,L

for a being Element of L holds a * (p *' p9) = p *' (a * p9)

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

for p, p9 being Series of n,L

for a being Element of L holds a * (p *' p9) = p *' (a * p9)

proof end;

definition

let n be Ordinal;

let b be bag of n;

let L be non empty ZeroStr ;

let p be Series of n,L;

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

for b9 being bag of n st b divides b9 holds

( b_{1} . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds

b_{1} . b9 = 0. L ) )

for b_{1}, b_{2} being Series of n,L st ( for b9 being bag of n st b divides b9 holds

( b_{1} . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds

b_{1} . b9 = 0. L ) ) ) & ( for b9 being bag of n st b divides b9 holds

( b_{2} . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds

b_{2} . b9 = 0. L ) ) ) holds

b_{1} = b_{2}

end;
let b be bag of n;

let L be non empty ZeroStr ;

let p be Series of n,L;

func b *' p -> Series of n,L means :Def1: :: POLYRED:def 1

for b9 being bag of n st b divides b9 holds

( it . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds

it . b9 = 0. L ) );

existence for b9 being bag of n st b divides b9 holds

( it . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds

it . b9 = 0. L ) );

ex b

for b9 being bag of n st b divides b9 holds

( b

b

proof end;

uniqueness for b

( b

b

( b

b

b

proof end;

:: deftheorem Def1 defines *' POLYRED:def 1 :

for n being Ordinal

for b being bag of n

for L being non empty ZeroStr

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

( b_{5} = b *' p iff for b9 being bag of n st b divides b9 holds

( b_{5} . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds

b_{5} . b9 = 0. L ) ) );

for n being Ordinal

for b being bag of n

for L being non empty ZeroStr

for p, b

( b

( b

b

Lm9: for n being Ordinal

for b, b9 being bag of n

for L being non empty ZeroStr

for p being Series of n,L holds (b *' p) . (b9 + b) = p . b9

proof end;

Lm10: for n being Ordinal

for L being non empty ZeroStr

for p being Polynomial of n,L

for b being bag of n holds Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p }

proof end;

registration

let n be Ordinal;

let b be bag of n;

let L be non empty ZeroStr ;

let p be finite-Support Series of n,L;

coherence

b *' p is finite-Support

end;
let b be bag of n;

let L be non empty ZeroStr ;

let p be finite-Support Series of n,L;

coherence

b *' p is finite-Support

proof end;

theorem :: POLYRED:13

theorem :: POLYRED:14

theorem Th15: :: POLYRED:15

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial ZeroStr

for p being non-zero Polynomial of n,L

for b being bag of n holds HT ((b *' p),T) = b + (HT (p,T))

for T being connected admissible TermOrder of n

for L being non trivial ZeroStr

for p being non-zero Polynomial of n,L

for b being bag of n holds HT ((b *' p),T) = b + (HT (p,T))

proof end;

theorem Th16: :: POLYRED:16

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty ZeroStr

for p being Polynomial of n,L

for b, b9 being bag of n st b9 in Support (b *' p) holds

b9 <= b + (HT (p,T)),T

for T being connected admissible TermOrder of n

for L being non empty ZeroStr

for p being Polynomial of n,L

for b, b9 being bag of n st b9 in Support (b *' p) holds

b9 <= b + (HT (p,T)),T

proof end;

theorem :: POLYRED:17

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

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

for T being connected TermOrder of n

for L being non empty ZeroStr

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

proof end;

theorem Th18: :: POLYRED:18

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p being Series of n,L

for b1, b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p)

for T being connected TermOrder of n

for L being non empty ZeroStr

for p being Series of n,L

for b1, b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p)

proof end;

theorem Th19: :: POLYRED:19

for n being Ordinal

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

for p being Polynomial of n,L

for a being Element of L holds Support (a * p) c= Support p

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

for p being Polynomial of n,L

for a being Element of L holds Support (a * p) c= Support p

proof end;

theorem :: POLYRED:20

for n being Ordinal

for L being non trivial domRing-like doubleLoopStr

for p being Polynomial of n,L

for a being non zero Element of L holds Support p c= Support (a * p)

for L being non trivial domRing-like doubleLoopStr

for p being Polynomial of n,L

for a being non zero Element of L holds Support p c= Support (a * p)

proof end;

theorem Th21: :: POLYRED:21

for n being Ordinal

for T being connected TermOrder of n

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

for p being Polynomial of n,L

for a being non zero Element of L holds HT ((a * p),T) = HT (p,T)

for T being connected TermOrder of n

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

for p being Polynomial of n,L

for a being non zero Element of L holds HT ((a * p),T) = HT (p,T)

proof end;

theorem Th22: :: POLYRED:22

for n being Ordinal

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

for p being Series of n,L

for b being bag of n

for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p

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

for p being Series of n,L

for b being bag of n

for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p

proof end;

theorem :: POLYRED:23

for n being Ordinal

for T being connected admissible TermOrder of n

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

for p being non-zero Polynomial of n,L

for q being Polynomial of n,L

for m being non-zero Monomial of n,L st HT (p,T) in Support q holds

HT ((m *' p),T) in Support (m *' q)

for T being connected admissible TermOrder of n

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

for p being non-zero Polynomial of n,L

for q being Polynomial of n,L

for m being non-zero Monomial of n,L st HT (p,T) in Support q holds

HT ((m *' p),T) in Support (m *' q)

proof end;

registration

let n be Ordinal;

let T be connected TermOrder of n;

coherence

RelStr(# (Bags n),T #) is connected

end;
let T be connected TermOrder of n;

coherence

RelStr(# (Bags n),T #) is connected

proof end;

registration

let n be Nat;

let T be admissible TermOrder of n;

coherence

RelStr(# (Bags n),T #) is well_founded

end;
let T be admissible TermOrder of n;

coherence

RelStr(# (Bags n),T #) is well_founded

proof end;

Lm11: for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p being Polynomial of n,L holds Support p in Fin the carrier of RelStr(# (Bags n),T #)

proof end;

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p, q be Polynomial of n,L;

end;
let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p, q be Polynomial of n,L;

:: deftheorem defines <= POLYRED:def 2 :

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p, q being Polynomial of n,L holds

( p <= q,T iff [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) );

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p, q being Polynomial of n,L holds

( p <= q,T iff [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) );

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p, q be Polynomial of n,L;

end;
let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p, q be Polynomial of n,L;

:: deftheorem defines < POLYRED:def 3 :

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p, q being Polynomial of n,L holds

( p < q,T iff ( p <= q,T & Support p <> Support q ) );

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p, q being Polynomial of n,L holds

( p < q,T iff ( p <= q,T & Support p <> Support q ) );

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p be Polynomial of n,L;

Support p is Element of Fin the carrier of RelStr(# (Bags n),T #) by Lm11;

end;
let T be connected TermOrder of n;

let L be non empty ZeroStr ;

let p be Polynomial of n,L;

func Support (p,T) -> Element of Fin the carrier of RelStr(# (Bags n),T #) equals :: POLYRED:def 4

Support p;

coherence Support p;

Support p is Element of Fin the carrier of RelStr(# (Bags n),T #) by Lm11;

:: deftheorem defines Support POLYRED:def 4 :

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p being Polynomial of n,L holds Support (p,T) = Support p;

for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p being Polynomial of n,L holds Support (p,T) = Support p;

theorem Th24: :: POLYRED:24

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial ZeroStr

for p being non-zero Polynomial of n,L holds PosetMax (Support (p,T)) = HT (p,T)

for T being connected TermOrder of n

for L being non trivial ZeroStr

for p being non-zero Polynomial of n,L holds PosetMax (Support (p,T)) = HT (p,T)

proof end;

theorem Th25: :: POLYRED:25

for n being Ordinal

for T being connected TermOrder of n

for L being non empty addLoopStr

for p being Polynomial of n,L holds p <= p,T by Lm11, ORDERS_1:3;

for T being connected TermOrder of n

for L being non empty addLoopStr

for p being Polynomial of n,L holds p <= p,T by Lm11, ORDERS_1:3;

Lm12: for n being Ordinal

for T being connected TermOrder of n

for L being non empty ZeroStr

for p being Polynomial of n,L holds 0_ (n,L) <= p,T

proof end;

theorem Th26: :: POLYRED:26

for n being Ordinal

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q being Polynomial of n,L holds

( ( p <= q,T & q <= p,T ) iff Support p = Support q )

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q being Polynomial of n,L holds

( ( p <= q,T & q <= p,T ) iff Support p = Support q )

proof end;

theorem Th27: :: POLYRED:27

for n being Ordinal

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds

p <= r,T

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds

p <= r,T

proof end;

theorem Th28: :: POLYRED:28

for n being Ordinal

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q being Polynomial of n,L holds

( p <= q,T or q <= p,T )

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q being Polynomial of n,L holds

( p <= q,T or q <= p,T )

proof end;

theorem Th29: :: POLYRED:29

for n being Ordinal

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q being Polynomial of n,L holds

( p <= q,T iff not q < p,T )

for T being connected TermOrder of n

for L being non empty addLoopStr

for p, q being Polynomial of n,L holds

( p <= q,T iff not q < p,T )

proof end;

Lm13: for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for b being bag of n st [(HT (p,T)),b] in T & b <> HT (p,T) holds

p . b = 0. L

proof end;

Lm14: for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L st HT (p,T) = EmptyBag n holds

Red (p,T) = 0_ (n,L)

proof end;

Lm15: for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p, q being Polynomial of n,L holds

( p < q,T iff ( ( p = 0_ (n,L) & q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T ) ) )

proof end;

theorem :: POLYRED:30

Lm16: for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p, q being Polynomial of n,L st q <> 0_ (n,L) & HT (p,T) = HT (q,T) & Red (p,T) <= Red (q,T),T holds

p <= q,T

proof end;

theorem Th31: :: POLYRED:31

for n being Nat

for T being connected admissible TermOrder of n

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

for P being non empty Subset of (Polynom-Ring (n,L)) ex p being Polynomial of n,L st

( p in P & ( for q being Polynomial of n,L st q in P holds

p <= q,T ) )

for T being connected admissible TermOrder of n

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

for P being non empty Subset of (Polynom-Ring (n,L)) ex p being Polynomial of n,L st

( p in P & ( for q being Polynomial of n,L st q in P holds

p <= q,T ) )

proof end;

theorem :: POLYRED:32

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p, q being Polynomial of n,L holds

( p < q,T iff ( ( p = 0_ (n,L) & q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T ) ) ) by Lm15;

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p, q being Polynomial of n,L holds

( p < q,T iff ( ( p = 0_ (n,L) & q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T ) ) ) by Lm15;

theorem Th33: :: POLYRED:33

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being non-zero Polynomial of n,L holds Red (p,T) < HM (p,T),T

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being non-zero Polynomial of n,L holds Red (p,T) < HM (p,T),T

proof end;

theorem Th34: :: POLYRED:34

for n being Ordinal

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds HM (p,T) <= p,T

for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds HM (p,T) <= p,T

proof end;

theorem Th35: :: POLYRED:35

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being non-zero Polynomial of n,L holds Red (p,T) < p,T

for T being connected admissible TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being non-zero Polynomial of n,L holds Red (p,T) < p,T

proof end;

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p, g be Polynomial of n,L;

let b be bag of n;

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p, g be Polynomial of n,L;

let b be bag of n;

:: deftheorem defines reduces_to POLYRED:def 5 :

for n being Ordinal

for T being connected TermOrder of n

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

for f, p, g being Polynomial of n,L

for b being bag of n holds

( f reduces_to g,p,b,T iff ( f <> 0_ (n,L) & p <> 0_ (n,L) & b in Support f & ex s being bag of n st

( s + (HT (p,T)) = b & g = f - (((f . b) / (HC (p,T))) * (s *' p)) ) ) );

for n being Ordinal

for T being connected TermOrder of n

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

for f, p, g being Polynomial of n,L

for b being bag of n holds

( f reduces_to g,p,b,T iff ( f <> 0_ (n,L) & p <> 0_ (n,L) & b in Support f & ex s being bag of n st

( s + (HT (p,T)) = b & g = f - (((f . b) / (HC (p,T))) * (s *' p)) ) ) );

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p, g be Polynomial of n,L;

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p, g be Polynomial of n,L;

:: deftheorem defines reduces_to POLYRED:def 6 :

for n being Ordinal

for T being connected TermOrder of n

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

for f, p, g being Polynomial of n,L holds

( f reduces_to g,p,T iff ex b being bag of n st f reduces_to g,p,b,T );

for n being Ordinal

for T being connected TermOrder of n

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

for f, p, g being Polynomial of n,L holds

( f reduces_to g,p,T iff ex b being bag of n st f reduces_to g,p,b,T );

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, g be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, g be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

pred f reduces_to g,P,T means :: POLYRED:def 7

ex p being Polynomial of n,L st

( p in P & f reduces_to g,p,T );

ex p being Polynomial of n,L st

( p in P & f reduces_to g,p,T );

:: deftheorem defines reduces_to POLYRED:def 7 :

for n being Ordinal

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) holds

( f reduces_to g,P,T iff ex p being Polynomial of n,L st

( p in P & f reduces_to g,p,T ) );

for n being Ordinal

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) holds

( f reduces_to g,P,T iff ex p being Polynomial of n,L st

( p in P & f reduces_to g,p,T ) );

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p be Polynomial of n,L;

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p be Polynomial of n,L;

pred f is_reducible_wrt p,T means :: POLYRED:def 8

ex g being Polynomial of n,L st f reduces_to g,p,T;

ex g being Polynomial of n,L st f reduces_to g,p,T;

:: deftheorem defines is_reducible_wrt POLYRED:def 8 :

for n being Ordinal

for T being connected TermOrder of n

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

for f, p being Polynomial of n,L holds

( f is_reducible_wrt p,T iff ex g being Polynomial of n,L st f reduces_to g,p,T );

for n being Ordinal

for T being connected TermOrder of n

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

for f, p being Polynomial of n,L holds

( f is_reducible_wrt p,T iff ex g being Polynomial of n,L st f reduces_to g,p,T );

notation

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p be Polynomial of n,L;

antonym f is_irreducible_wrt p,T for f is_reducible_wrt p,T;

antonym f is_in_normalform_wrt p,T for f is_reducible_wrt p,T;

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p be Polynomial of n,L;

antonym f is_irreducible_wrt p,T for f is_reducible_wrt p,T;

antonym f is_in_normalform_wrt p,T for f is_reducible_wrt p,T;

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

pred f is_reducible_wrt P,T means :: POLYRED:def 9

ex g being Polynomial of n,L st f reduces_to g,P,T;

ex g being Polynomial of n,L st f reduces_to g,P,T;

:: deftheorem defines is_reducible_wrt POLYRED:def 9 :

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) holds

( f is_reducible_wrt P,T iff ex g being Polynomial of n,L st f reduces_to g,P,T );

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) holds

( f is_reducible_wrt P,T iff ex g being Polynomial of n,L st f reduces_to g,P,T );

notation

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

antonym f is_irreducible_wrt P,T for f is_reducible_wrt P,T;

antonym f is_in_normalform_wrt P,T for f is_reducible_wrt P,T;

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

antonym f is_irreducible_wrt P,T for f is_reducible_wrt P,T;

antonym f is_in_normalform_wrt P,T for f is_reducible_wrt P,T;

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p, g be Polynomial of n,L;

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p, g be Polynomial of n,L;

:: deftheorem defines top_reduces_to POLYRED:def 10 :

for n being Ordinal

for T being connected TermOrder of n

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

for f, p, g being Polynomial of n,L holds

( f top_reduces_to g,p,T iff f reduces_to g,p, HT (f,T),T );

for n being Ordinal

for T being connected TermOrder of n

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

for f, p, g being Polynomial of n,L holds

( f top_reduces_to g,p,T iff f reduces_to g,p, HT (f,T),T );

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p be Polynomial of n,L;

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f, p be Polynomial of n,L;

pred f is_top_reducible_wrt p,T means :: POLYRED:def 11

ex g being Polynomial of n,L st f top_reduces_to g,p,T;

ex g being Polynomial of n,L st f top_reduces_to g,p,T;

:: deftheorem defines is_top_reducible_wrt POLYRED:def 11 :

for n being Ordinal

for T being connected TermOrder of n

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

for f, p being Polynomial of n,L holds

( f is_top_reducible_wrt p,T iff ex g being Polynomial of n,L st f top_reduces_to g,p,T );

for n being Ordinal

for T being connected TermOrder of n

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

for f, p being Polynomial of n,L holds

( f is_top_reducible_wrt p,T iff ex g being Polynomial of n,L st f top_reduces_to g,p,T );

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let f be Polynomial of n,L;

let P be Subset of (Polynom-Ring (n,L));

pred f is_top_reducible_wrt P,T means :: POLYRED:def 12

ex p being Polynomial of n,L st

( p in P & f is_top_reducible_wrt p,T );

ex p being Polynomial of n,L st

( p in P & f is_top_reducible_wrt p,T );

:: deftheorem defines is_top_reducible_wrt POLYRED:def 12 :

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) holds

( f is_top_reducible_wrt P,T iff ex p being Polynomial of n,L st

( p in P & f is_top_reducible_wrt p,T ) );

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) holds

( f is_top_reducible_wrt P,T iff ex p being Polynomial of n,L st

( p in P & f is_top_reducible_wrt p,T ) );

theorem :: POLYRED:36

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

for p being non-zero Polynomial of n,L holds

( f is_reducible_wrt p,T iff ex b being bag of n st

( b in Support f & HT (p,T) divides b ) )

for T being connected TermOrder of n

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

for f being Polynomial of n,L

for p being non-zero Polynomial of n,L holds

( f is_reducible_wrt p,T iff ex b being bag of n st

( b in Support f & HT (p,T) divides b ) )

proof end;

Lm17: for n being Ordinal

for T being connected TermOrder of n

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

for f, p, g being Polynomial of n,L

for b being bag of n st f reduces_to g,p,b,T holds

not b in Support g

proof end;

theorem Th37: :: POLYRED:37

for n being Ordinal

for T being connected TermOrder of n

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

for p being Polynomial of n,L holds 0_ (n,L) is_irreducible_wrt p,T

for T being connected TermOrder of n

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

for p being Polynomial of n,L holds 0_ (n,L) is_irreducible_wrt p,T

proof end;

theorem :: POLYRED:38

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, p being Polynomial of n,L

for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds

HT ((m *' p),T) in Support f

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, p being Polynomial of n,L

for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds

HT ((m *' p),T) in Support f

proof end;

theorem :: POLYRED:39

for n being Ordinal

for T being connected TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, p, g being Polynomial of n,L

for b being bag of n st f reduces_to g,p,b,T holds

not b in Support g by Lm17;

for T being connected TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, p, g being Polynomial of n,L

for b being bag of n st f reduces_to g,p,b,T holds

not b in Support g by Lm17;

theorem Th40: :: POLYRED:40

for n being Ordinal

for T being connected admissible TermOrder of n

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

for f, p, g being Polynomial of n,L

for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds

( b9 in Support g iff b9 in Support f )

for T being connected admissible TermOrder of n

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

for f, p, g being Polynomial of n,L

for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds

( b9 in Support g iff b9 in Support f )

proof end;

theorem Th41: :: POLYRED:41

for n being Ordinal

for T being connected admissible TermOrder of n

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

for f, p, g being Polynomial of n,L

for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds

f . b9 = g . b9

for T being connected admissible TermOrder of n

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

for f, p, g being Polynomial of n,L

for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds

f . b9 = g . b9

proof end;

theorem Th42: :: POLYRED:42

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds

for b being bag of n st b in Support g holds

b <= HT (f,T),T

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds

for b being bag of n st b in Support g holds

b <= HT (f,T),T

proof end;

theorem Th43: :: POLYRED:43

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds

g < f,T

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds

g < f,T

proof end;

definition

let n be Ordinal;

let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let P be Subset of (Polynom-Ring (n,L));

ex b_{1} being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) st

for p, q being Polynomial of n,L holds

( [p,q] in b_{1} iff p reduces_to q,P,T )

for b_{1}, b_{2} being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) st ( for p, q being Polynomial of n,L holds

( [p,q] in b_{1} iff p reduces_to q,P,T ) ) & ( for p, q being Polynomial of n,L holds

( [p,q] in b_{2} iff p reduces_to q,P,T ) ) holds

b_{1} = b_{2}

end;
let T be connected TermOrder of n;

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let P be Subset of (Polynom-Ring (n,L));

func PolyRedRel (P,T) -> Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) means :Def13: :: POLYRED:def 13

for p, q being Polynomial of n,L holds

( [p,q] in it iff p reduces_to q,P,T );

existence for p, q being Polynomial of n,L holds

( [p,q] in it iff p reduces_to q,P,T );

ex b

for p, q being Polynomial of n,L holds

( [p,q] in b

proof end;

uniqueness for b

( [p,q] in b

( [p,q] in b

b

proof end;

:: deftheorem Def13 defines PolyRedRel POLYRED:def 13 :

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for b_{5} being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) holds

( b_{5} = PolyRedRel (P,T) iff for p, q being Polynomial of n,L holds

( [p,q] in b_{5} iff p reduces_to q,P,T ) );

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for b

( b

( [p,q] in b

Lm18: for n being Ordinal

for T being connected TermOrder of n

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

for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds

( f <> 0_ (n,L) & p <> 0_ (n,L) )

proof end;

theorem :: POLYRED:44

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, g being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, g being Polynomial of n,L

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )

proof end;

registration

let n be Nat;

let T be connected admissible TermOrder of n;

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

let P be Subset of (Polynom-Ring (n,L));

coherence

PolyRedRel (P,T) is strongly-normalizing

end;
let T be connected admissible TermOrder of n;

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

let P be Subset of (Polynom-Ring (n,L));

coherence

PolyRedRel (P,T) is strongly-normalizing

proof end;

theorem Th45: :: POLYRED:45

for n being Nat

for T being connected admissible TermOrder of n

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative left_zeroed doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f, h being Polynomial of n,L st f in P holds

PolyRedRel (P,T) reduces h *' f, 0_ (n,L)

for T being connected admissible TermOrder of n

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative left_zeroed doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f, h being Polynomial of n,L st f in P holds

PolyRedRel (P,T) reduces h *' f, 0_ (n,L)

proof end;

theorem Th46: :: POLYRED:46

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L

for m being non-zero Monomial of n,L st f reduces_to g,P,T holds

m *' f reduces_to m *' g,P,T

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L

for m being non-zero Monomial of n,L st f reduces_to g,P,T holds

m *' f reduces_to m *' g,P,T

proof end;

theorem Th47: :: POLYRED:47

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L

for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds

PolyRedRel (P,T) reduces m *' f,m *' g

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L

for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds

PolyRedRel (P,T) reduces m *' f,m *' g

proof end;

theorem :: POLYRED:48

for n being Ordinal

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f being Polynomial of n,L

for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

PolyRedRel (P,T) reduces m *' f, 0_ (n,L)

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L))

for f being Polynomial of n,L

for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

PolyRedRel (P,T) reduces m *' f, 0_ (n,L)

proof end;

theorem Th49: :: POLYRED:49

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel (P,T) reduces h,h1 holds

ex f1, g1 being Polynomial of n,L st

( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel (P,T) reduces h,h1 holds

ex f1, g1 being Polynomial of n,L st

( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )

proof end;

theorem Th50: :: POLYRED:50

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds

f,g are_convergent_wrt PolyRedRel (P,T)

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds

f,g are_convergent_wrt PolyRedRel (P,T)

proof end;

theorem Th51: :: POLYRED:51

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds

f,g are_convertible_wrt PolyRedRel (P,T)

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds

f,g are_convertible_wrt PolyRedRel (P,T)

proof end;

:: deftheorem defines are_congruent_mod POLYRED:def 14 :

for R being non empty addLoopStr

for I being Subset of R

for a, b being Element of R holds

( a,b are_congruent_mod I iff a - b in I );

for R being non empty addLoopStr

for I being Subset of R

for a, b being Element of R holds

( a,b are_congruent_mod I iff a - b in I );

theorem :: POLYRED:52

for R being non empty right_complementable right-distributive add-associative right_zeroed left_zeroed doubleLoopStr

for I being non empty right-ideal Subset of R

for a being Element of R holds a,a are_congruent_mod I

for I being non empty right-ideal Subset of R

for a being Element of R holds a,a are_congruent_mod I

proof end;

theorem Th53: :: POLYRED:53

for R being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr

for I being non empty right-ideal Subset of R

for a, b being Element of R st a,b are_congruent_mod I holds

b,a are_congruent_mod I

for I being non empty right-ideal Subset of R

for a, b being Element of R st a,b are_congruent_mod I holds

b,a are_congruent_mod I

proof end;

theorem Th54: :: POLYRED:54

for R being non empty right_complementable add-associative right_zeroed addLoopStr

for I being non empty add-closed Subset of R

for a, b, c being Element of R st a,b are_congruent_mod I & b,c are_congruent_mod I holds

a,c are_congruent_mod I

for I being non empty add-closed Subset of R

for a, b, c being Element of R st a,b are_congruent_mod I & b,c are_congruent_mod I holds

a,c are_congruent_mod I

proof end;

theorem :: POLYRED:55

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

for I being non empty add-closed Subset of R

for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds

a + c,b + d are_congruent_mod I

for I being non empty add-closed Subset of R

for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds

a + c,b + d are_congruent_mod I

proof end;

theorem :: POLYRED:56

for R being non empty right_complementable distributive add-associative right_zeroed commutative doubleLoopStr

for I being non empty add-closed right-ideal Subset of R

for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds

a * c,b * d are_congruent_mod I

for I being non empty add-closed right-ideal Subset of R

for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds

a * c,b * d are_congruent_mod I

proof end;

Lm19: for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f being non-zero Polynomial of n,L

for g being Polynomial of n,L

for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds

f9,g9 are_congruent_mod P -Ideal

proof end;

theorem Th57: :: POLYRED:57

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Element of (Polynom-Ring (n,L)) st f,g are_convertible_wrt PolyRedRel (P,T) holds

f,g are_congruent_mod P -Ideal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Element of (Polynom-Ring (n,L)) st f,g are_convertible_wrt PolyRedRel (P,T) holds

f,g are_congruent_mod P -Ideal

proof end;

Lm20: for n being Nat

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being non empty Subset of (Polynom-Ring (n,L))

for f, p, h being Element of (Polynom-Ring (n,L)) st p in P & p <> 0_ (n,L) & h <> 0_ (n,L) holds

f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)

proof end;

theorem :: POLYRED:58

for n being Nat

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being non empty Subset of (Polynom-Ring (n,L))

for f, g being Element of (Polynom-Ring (n,L)) st f,g are_congruent_mod P -Ideal holds

f,g are_convertible_wrt PolyRedRel (P,T)

for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for P being non empty Subset of (Polynom-Ring (n,L))

for f, g being Element of (Polynom-Ring (n,L)) st f,g are_congruent_mod P -Ideal holds

f,g are_convertible_wrt PolyRedRel (P,T)

proof end;

theorem Th59: :: POLYRED:59

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds

f - g in P -Ideal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds

f - g in P -Ideal

proof end;

theorem :: POLYRED:60

for n being Ordinal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f being Polynomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f in P -Ideal

for T being connected TermOrder of n

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

for P being Subset of (Polynom-Ring (n,L))

for f being Polynomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f in P -Ideal

proof end;