:: by Christoph Schwarzweller

::

:: Received June 11, 2003

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

theorem :: GROEB_2:1

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being FinSequence of L

for n being Element of NAT st ( for k being Element of NAT st k in dom p & k > n holds

p . k = 0. L ) holds

Sum p = Sum (p | n)

for p being FinSequence of L

for n being Element of NAT st ( for k being Element of NAT st k in dom p & k > n holds

p . k = 0. L ) holds

Sum p = Sum (p | n)

proof end;

theorem :: GROEB_2:2

for L being non empty Abelian add-associative right_zeroed addLoopStr

for f being FinSequence of L

for i, j being Element of NAT holds Sum (Swap (f,i,j)) = Sum f

for f being FinSequence of L

for i, j being Element of NAT holds Sum (Swap (f,i,j)) = Sum f

proof end;

definition

let X be set ;

let b1, b2 be bag of X;

assume A1: b2 divides b1 ;

existence

ex b_{1} being bag of X st b2 + b_{1} = b1
by A1, TERMORD:1;

uniqueness

for b_{1}, b_{2} being bag of X st b2 + b_{1} = b1 & b2 + b_{2} = b1 holds

b_{1} = b_{2}

end;
let b1, b2 be bag of X;

assume A1: b2 divides b1 ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def1 defines / GROEB_2:def 1 :

for X being set

for b1, b2 being bag of X st b2 divides b1 holds

for b_{4} being bag of X holds

( b_{4} = b1 / b2 iff b2 + b_{4} = b1 );

for X being set

for b1, b2 being bag of X st b2 divides b1 holds

for b

( b

definition

let X be set ;

let b1, b2 be bag of X;

ex b_{1} being bag of X st

for k being object holds b_{1} . k = max ((b1 . k),(b2 . k))

for b_{1}, b_{2} being bag of X st ( for k being object holds b_{1} . k = max ((b1 . k),(b2 . k)) ) & ( for k being object holds b_{2} . k = max ((b1 . k),(b2 . k)) ) holds

b_{1} = b_{2}

for b_{1}, b1, b2 being bag of X st ( for k being object holds b_{1} . k = max ((b1 . k),(b2 . k)) ) holds

for k being object holds b_{1} . k = max ((b2 . k),(b1 . k))
;

idempotence

for b1 being bag of X

for k being object holds b1 . k = max ((b1 . k),(b1 . k)) ;

end;
let b1, b2 be bag of X;

func lcm (b1,b2) -> bag of X means :Def2: :: GROEB_2:def 2

for k being object holds it . k = max ((b1 . k),(b2 . k));

existence for k being object holds it . k = max ((b1 . k),(b2 . k));

ex b

for k being object holds b

proof end;

uniqueness for b

b

proof end;

commutativity for b

for k being object holds b

idempotence

for b1 being bag of X

for k being object holds b1 . k = max ((b1 . k),(b1 . k)) ;

:: deftheorem Def2 defines lcm GROEB_2:def 2 :

for X being set

for b1, b2, b_{4} being bag of X holds

( b_{4} = lcm (b1,b2) iff for k being object holds b_{4} . k = max ((b1 . k),(b2 . k)) );

for X being set

for b1, b2, b

( b

:: exercise 5.45, p. 211

definition

let X be set ;

let b1, b2 be bag of X;

end;
let b1, b2 be bag of X;

pred b1,b2 are_disjoint means :: GROEB_2:def 3

for i being object holds

( b1 . i = 0 or b2 . i = 0 );

for i being object holds

( b1 . i = 0 or b2 . i = 0 );

:: deftheorem defines are_disjoint GROEB_2:def 3 :

for X being set

for b1, b2 being bag of X holds

( b1,b2 are_disjoint iff for i being object holds

( b1 . i = 0 or b2 . i = 0 ) );

for X being set

for b1, b2 being bag of X holds

( b1,b2 are_disjoint iff for i being object holds

( b1 . i = 0 or b2 . i = 0 ) );

notation
end;

:: exercise 5.45, p. 211

theorem Th4: :: GROEB_2:4

for X being set

for b1, b2, b3 being bag of X st b1 divides b3 & b2 divides b3 holds

lcm (b1,b2) divides b3

for b1, b2, b3 being bag of X st b1 divides b3 & b2 divides b3 holds

lcm (b1,b2) divides b3

proof end;

:: exercise 5.45, p. 211

theorem :: GROEB_2:8

for X being set

for b1, b2, b3 being bag of X st b1 divides lcm (b2,b3) holds

lcm (b2,b1) divides lcm (b2,b3)

for b1, b2, b3 being bag of X st b1 divides lcm (b2,b3) holds

lcm (b2,b1) divides lcm (b2,b3)

proof end;

:: exercise 5.69 (i) ==> (ii), p. 223

theorem :: GROEB_2:9

for X being set

for b1, b2, b3 being bag of X st lcm (b2,b1) divides lcm (b2,b3) holds

lcm (b1,b3) divides lcm (b2,b3)

for b1, b2, b3 being bag of X st lcm (b2,b1) divides lcm (b2,b3) holds

lcm (b1,b3) divides lcm (b2,b3)

proof end;

:: exercise 5.69 (ii) ==> (iii), p. 223

theorem :: GROEB_2:10

for n being set

for b1, b2, b3 being bag of n st lcm (b1,b3) divides lcm (b2,b3) holds

b1 divides lcm (b2,b3)

for b1, b2, b3 being bag of n st lcm (b1,b3) divides lcm (b2,b3) holds

b1 divides lcm (b2,b3)

proof end;

:: exercise 5.69 (iii) ==> (i), p. 223

theorem :: GROEB_2:11

for n being Element of NAT

for T being connected admissible TermOrder of n

for P being non empty Subset of (Bags n) ex b being bag of n st

( b in P & ( for b9 being bag of n st b9 in P holds

b <= b9,T ) )

for T being connected admissible TermOrder of n

for P being non empty Subset of (Bags n) ex b being bag of n st

( b in P & ( for b9 being bag of n st b9 in P holds

b <= b9,T ) )

proof end;

registration

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

let a be non zero Element of L;

coherence

not - a is zero

end;
let a be non zero Element of L;

coherence

not - a is zero

proof end;

registration

let X be set ;

let L be non empty add-cancelable distributive right_zeroed left_zeroed doubleLoopStr ;

let m be Monomial of X,L;

let a be Element of L;

coherence

a * m is monomial-like

end;
let L be non empty add-cancelable distributive right_zeroed left_zeroed doubleLoopStr ;

let m be Monomial of X,L;

let a be Element of L;

coherence

a * m is monomial-like

proof end;

registration

let n be Ordinal;

let L be non trivial add-cancelable distributive right_zeroed domRing-like left_zeroed doubleLoopStr ;

let p be non-zero Polynomial of n,L;

let a be non zero Element of L;

coherence

a * p is non-zero

end;
let L be non trivial add-cancelable distributive right_zeroed domRing-like left_zeroed doubleLoopStr ;

let p be non-zero Polynomial of n,L;

let a be non zero Element of L;

coherence

a * p is non-zero

proof end;

theorem Th12: :: GROEB_2:12

for n being Ordinal

for L being non empty right-distributive right_zeroed doubleLoopStr

for p, q being Series of n,L

for b being bag of n holds b *' (p + q) = (b *' p) + (b *' q)

for L being non empty right-distributive right_zeroed doubleLoopStr

for p, q being Series of n,L

for b being bag of n holds b *' (p + q) = (b *' p) + (b *' q)

proof end;

theorem Th13: :: GROEB_2:13

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L

for b being bag of n holds b *' (- p) = - (b *' p)

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Series of n,L

for b being bag of n holds b *' (- p) = - (b *' p)

proof end;

theorem Th14: :: GROEB_2:14

for n being Ordinal

for L being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr

for p being Series of n,L

for b being bag of n

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

for L being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr

for p being Series of n,L

for b being bag of n

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

proof end;

theorem Th15: :: GROEB_2:15

for n being Ordinal

for L being non empty right-distributive doubleLoopStr

for p, q being Series of n,L

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

for L being non empty right-distributive doubleLoopStr

for p, q being Series of n,L

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

proof end;

theorem Th16: :: GROEB_2:16

for X being set

for L being non empty right_complementable add-associative right_zeroed doubleLoopStr

for a being Element of L holds - (a | (X,L)) = (- a) | (X,L)

for L being non empty right_complementable add-associative right_zeroed doubleLoopStr

for a being Element of L holds - (a | (X,L)) = (- a) | (X,L)

proof end;

Lm1: 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 g being object

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

g is Polynomial of n,L

proof end;

theorem Th17: :: GROEB_2:17

for n being Element of 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 Subset of (Polynom-Ring (n,L)) st ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds

for m1, m2 being Monomial of n,L st HM ((m1 *' p1),T) = HM ((m2 *' p2),T) holds

PolyRedRel (P,T) reduces (m1 *' p1) - (m2 *' p2), 0_ (n,L) ) holds

P is_Groebner_basis_wrt 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)) st ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds

for m1, m2 being Monomial of n,L st HM ((m1 *' p1),T) = HM ((m2 *' p2),T) holds

PolyRedRel (P,T) reduces (m1 *' p1) - (m2 *' p2), 0_ (n,L) ) holds

P is_Groebner_basis_wrt 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 p1, p2 be Polynomial of n,L;

((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)) is 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 p1, p2 be Polynomial of n,L;

func S-Poly (p1,p2,T) -> Polynomial of n,L equals :: GROEB_2:def 4

((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));

coherence ((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));

((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)) is Polynomial of n,L ;

:: deftheorem defines S-Poly GROEB_2:def 4 :

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 p1, p2 being Polynomial of n,L holds S-Poly (p1,p2,T) = ((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));

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 p1, p2 being Polynomial of n,L holds S-Poly (p1,p2,T) = ((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));

Lm2: for L being non empty add-cancelable right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr

for P being Subset of L

for p being Element of L st p in P holds

p in P -Ideal

proof end;

Lm3: for n being Ordinal

for T being connected TermOrder of n

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

for p, q being Polynomial of n,L

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

f - g = p - q

proof end;

theorem Th18: :: GROEB_2:18

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 p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds

S-Poly (p1,p2,T) 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 p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds

S-Poly (p1,p2,T) in P -Ideal

proof end;

theorem Th19: :: GROEB_2:19

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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)

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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)

proof end;

:: exercise 5.47 (i), p. 211

theorem Th20: :: GROEB_2:20

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

( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )

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

( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )

proof end;

theorem :: GROEB_2:21

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 p1, p2 being Polynomial of n,L holds

( S-Poly (p1,p2,T) = 0_ (n,L) or HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T )

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 p1, p2 being Polynomial of n,L holds

( S-Poly (p1,p2,T) = 0_ (n,L) or HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T )

proof end;

:: exercise 5.47 (ii), p. 211

theorem :: GROEB_2:22

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 p1, p2 being non-zero Polynomial of n,L st HT (p2,T) divides HT (p1,T) holds

(HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,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 p1, p2 being non-zero Polynomial of n,L st HT (p2,T) divides HT (p1,T) holds

(HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T

proof end;

:: exercise 5.47 (iii), p. 211

theorem :: GROEB_2:23

for n being Element of 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 G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds

for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 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 G being Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds

for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L)

proof end;

:: theorem 5.48 (i) ==> (ii), p. 211

theorem :: GROEB_2:24

for n being Element of 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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 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 G being Subset of (Polynom-Ring (n,L)) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds

h = 0_ (n,L) ) holds

for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

proof end;

:: theorem 5.48 (ii) ==> (iii), p. 211

theorem Th25: :: GROEB_2:25

for n being Element of 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_wrt 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_wrt T

proof end;

:: theorem 5.48 (iii) ==> (i), p. 211

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

{ (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } is 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 P be Subset of (Polynom-Ring (n,L));

func S-Poly (P,T) -> Subset of (Polynom-Ring (n,L)) equals :: GROEB_2:def 5

{ (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;

coherence { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;

{ (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } is Subset of (Polynom-Ring (n,L))

proof end;

:: deftheorem defines S-Poly GROEB_2: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 P being Subset of (Polynom-Ring (n,L)) holds S-Poly (P,T) = { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in 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 P being Subset of (Polynom-Ring (n,L)) holds S-Poly (P,T) = { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;

registration

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 finite Subset of (Polynom-Ring (n,L));

coherence

S-Poly (P,T) is finite

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 finite Subset of (Polynom-Ring (n,L));

coherence

S-Poly (P,T) is finite

proof end;

theorem :: GROEB_2:26

for n being Element of 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt T

proof end;

theorem :: GROEB_2:27

for L being non empty multLoopStr

for P being non empty Subset of L

for A being LeftLinearCombination of P

for i being Element of NAT holds A | i is LeftLinearCombination of P

for P being non empty Subset of L

for A being LeftLinearCombination of P

for i being Element of NAT holds A | i is LeftLinearCombination of P

proof end;

theorem :: GROEB_2:28

for L being non empty multLoopStr

for P being non empty Subset of L

for A being LeftLinearCombination of P

for i being Element of NAT holds A /^ i is LeftLinearCombination of P

for P being non empty Subset of L

for A being LeftLinearCombination of P

for i being Element of NAT holds A /^ i is LeftLinearCombination of P

proof end;

theorem :: GROEB_2:29

for L being non empty multLoopStr

for P, Q being non empty Subset of L

for A being LeftLinearCombination of P st P c= Q holds

A is LeftLinearCombination of Q

for P, Q being non empty Subset of L

for A being LeftLinearCombination of P st P c= Q holds

A is LeftLinearCombination of Q

proof end;

definition

let n be Ordinal;

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

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

let A, B be LeftLinearCombination of P;

:: original: ^

redefine func A ^ B -> LeftLinearCombination of P;

coherence

A ^ B is LeftLinearCombination of P

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

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

let A, B be LeftLinearCombination of P;

:: original: ^

redefine func A ^ B -> LeftLinearCombination of P;

coherence

A ^ B is LeftLinearCombination of P

proof end;

definition

let n be Ordinal;

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

let f be Polynomial of n,L;

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

let A be LeftLinearCombination of P;

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

let f be Polynomial of n,L;

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

let A be LeftLinearCombination of P;

pred A is_MonomialRepresentation_of f means :: GROEB_2:def 6

( Sum A = f & ( for i being Element of NAT st i in dom A holds

ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & A /. i = m *' p ) ) );

( Sum A = f & ( for i being Element of NAT st i in dom A holds

ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & A /. i = m *' p ) ) );

:: deftheorem defines is_MonomialRepresentation_of GROEB_2:def 6 :

for n being Ordinal

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P holds

( A is_MonomialRepresentation_of f iff ( Sum A = f & ( for i being Element of NAT st i in dom A holds

ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & A /. i = m *' p ) ) ) );

for n being Ordinal

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P holds

( A is_MonomialRepresentation_of f iff ( Sum A = f & ( for i being Element of NAT st i in dom A holds

ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & A /. i = m *' p ) ) ) );

theorem :: GROEB_2:30

for n being Ordinal

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st

( i in dom A & A /. i = m *' p ) }

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st

( i in dom A & A /. i = m *' p ) }

proof end;

theorem :: GROEB_2:31

for n being Ordinal

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds

A ^ B is_MonomialRepresentation_of f + g

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds

A ^ B is_MonomialRepresentation_of f + g

proof end;

Lm4: for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

proof end;

definition

let n be Ordinal;

let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

let A be LeftLinearCombination of P;

let b be bag of n;

end;
let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

let A be LeftLinearCombination of P;

let b be bag of n;

:: deftheorem defines is_Standard_Representation_of GROEB_2:def 7 :

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P

for b being bag of n holds

( A is_Standard_Representation_of f,P,b,T iff ( Sum A = f & ( for i being Element of NAT st i in dom A holds

ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & A /. i = m *' p & HT ((m *' p),T) <= b,T ) ) ) );

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P

for b being bag of n holds

( A is_Standard_Representation_of f,P,b,T iff ( Sum A = f & ( for i being Element of NAT st i in dom A holds

ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & A /. i = m *' p & HT ((m *' p),T) <= b,T ) ) ) );

definition

let n be Ordinal;

let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

let A be LeftLinearCombination of P;

end;
let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

let A be LeftLinearCombination of P;

pred A is_Standard_Representation_of f,P,T means :: GROEB_2:def 8

A is_Standard_Representation_of f,P, HT (f,T),T;

A is_Standard_Representation_of f,P, HT (f,T),T;

:: deftheorem defines is_Standard_Representation_of GROEB_2:def 8 :

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P holds

( A is_Standard_Representation_of f,P,T iff A is_Standard_Representation_of f,P, HT (f,T),T );

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P holds

( A is_Standard_Representation_of f,P,T iff A is_Standard_Representation_of f,P, HT (f,T),T );

definition

let n be Ordinal;

let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

let b be bag of n;

end;
let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

let b be bag of n;

pred f has_a_Standard_Representation_of P,b,T means :: GROEB_2:def 9

ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T;

ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T;

:: deftheorem defines has_a_Standard_Representation_of GROEB_2:def 9 :

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for b being bag of n holds

( f has_a_Standard_Representation_of P,b,T iff ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T );

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for b being bag of n holds

( f has_a_Standard_Representation_of P,b,T iff ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T );

definition

let n be Ordinal;

let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

end;
let T be connected TermOrder of n;

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

let f be Polynomial of n,L;

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

pred f has_a_Standard_Representation_of P,T means :: GROEB_2:def 10

ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T;

ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T;

:: deftheorem defines has_a_Standard_Representation_of GROEB_2:def 10 :

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

( f has_a_Standard_Representation_of P,T iff ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T );

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

( f has_a_Standard_Representation_of P,T iff ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T );

theorem Th32: :: GROEB_2:32

for n being Ordinal

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P

for b being bag of n st A is_Standard_Representation_of f,P,b,T holds

A is_MonomialRepresentation_of f

for T being connected TermOrder of n

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

for f being Polynomial of n,L

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

for A being LeftLinearCombination of P

for b being bag of n st A is_Standard_Representation_of f,P,b,T holds

A is_MonomialRepresentation_of f

proof end;

Lm5: 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 f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds

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

ex A being LeftLinearCombination of P st

( f9 = g9 + (Sum A) & ( for i being Element of NAT st i in dom A holds

ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & A . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) ) )

proof end;

theorem :: GROEB_2:33

for n being Ordinal

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P

for b being bag of n st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ B is_Standard_Representation_of f + g,P,b,T

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P

for b being bag of n st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ B is_Standard_Representation_of f + g,P,b,T

proof end;

theorem :: GROEB_2:34

for n being Ordinal

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P

for b being bag of n

for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds

B is_Standard_Representation_of f - g,P,b,T

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P

for b being bag of n

for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds

B is_Standard_Representation_of f - g,P,b,T

proof end;

theorem :: GROEB_2:35

for n being Ordinal

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P

for b being bag of n

for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A /^ i & g = Sum (A | i) & i <= len A holds

B is_Standard_Representation_of f - g,P,b,T

for T being connected TermOrder of n

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

for f, g being Polynomial of n,L

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

for A, B being LeftLinearCombination of P

for b being bag of n

for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A /^ i & g = Sum (A | i) & i <= len A holds

B is_Standard_Representation_of f - g,P,b,T

proof end;

theorem Th36: :: GROEB_2:36

for n being Ordinal

for T being connected TermOrder of n

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

for f being non-zero Polynomial of n,L

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

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

for T being connected TermOrder of n

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

for f being non-zero Polynomial of n,L

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

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

proof end;

theorem Th37: :: GROEB_2:37

for n being Ordinal

for T being connected TermOrder of n

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

for f being non-zero Polynomial of n,L

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

for A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),T) )

for T being connected TermOrder of n

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

for f being non-zero Polynomial of n,L

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

for A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),T) )

proof end;

theorem Th38: :: GROEB_2: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 being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of 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 f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

proof end;

:: lemma 5.60, p. 218

theorem Th39: :: GROEB_2:39

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 being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

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 being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

proof end;

:: lemma 5.61, p. 218

theorem :: GROEB_2:40

for n being Element of 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 G being non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,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 G being non empty Subset of (Polynom-Ring (n,L)) holds

( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds

f has_a_Standard_Representation_of G,T )

proof end;