let n be Element of NAT ; :: thesis: 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 I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T
let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T
A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
per cases ( I = {(0_ (n,L))} or I <> {(0_ (n,L))} ) ;
suppose A2: I = {(0_ (n,L))} ; :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T
set G = {(0_ (n,L))};
set R = PolyRedRel ({(0_ (n,L))},T);
take {(0_ (n,L))} ; :: thesis: {(0_ (n,L))} is_Groebner_basis_of I,T
now :: thesis: for a, b, c being object st [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) holds
b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)
let a, b, c be object ; :: thesis: ( [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) implies b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) )
assume that
A3: [a,b] in PolyRedRel ({(0_ (n,L))},T) and
[a,c] in PolyRedRel ({(0_ (n,L))},T) ; :: thesis: b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)
consider p, q being object such that
A4: p in NonZero (Polynom-Ring (n,L)) and
A5: q in the carrier of (Polynom-Ring (n,L)) and
A6: [a,b] = [p,q] by ;
reconsider q = q as Polynomial of n,L by ;
not p in {(0_ (n,L))} by ;
then p <> 0_ (n,L) by TARSKI:def 1;
then reconsider p = p as non-zero Polynomial of n,L by ;
p reduces_to q,{(0_ (n,L))},T by ;
then consider g being Polynomial of n,L such that
A7: g in {(0_ (n,L))} and
A8: p reduces_to q,g,T by POLYRED:def 7;
g = 0_ (n,L) by ;
then p is_reducible_wrt 0_ (n,L),T by ;
hence b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) by Lm3; :: thesis: verum
end;
then A9: PolyRedRel ({(0_ (n,L))},T) is locally-confluent by REWRITE1:def 24;
{(0_ (n,L))} -Ideal = I by ;
hence {(0_ (n,L))} is_Groebner_basis_of I,T by A9; :: thesis: verum
end;
suppose A10: I <> {(0_ (n,L))} ; :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T
ex q being Element of I st q <> 0_ (n,L)
proof
assume A11: for q being Element of I holds not q <> 0_ (n,L) ; :: thesis: contradiction
A12: now :: thesis: for u being object st u in {(0_ (n,L))} holds
u in I
let u be object ; :: thesis: ( u in {(0_ (n,L))} implies u in I )
assume u in {(0_ (n,L))} ; :: thesis: u in I
then A13: u = 0_ (n,L) by TARSKI:def 1;
hence u in I ; :: thesis: verum
end;
now :: thesis: for u being object st u in I holds
u in {(0_ (n,L))}
let u be object ; :: thesis: ( u in I implies u in {(0_ (n,L))} )
assume u in I ; :: thesis: u in {(0_ (n,L))}
then u = 0_ (n,L) by A11;
hence u in {(0_ (n,L))} by TARSKI:def 1; :: thesis: verum
end;
hence contradiction by A10, A12, TARSKI:2; :: thesis: verum
end;
then consider q being Element of I such that
A14: q <> 0_ (n,L) ;
set R = RelStr(# (Bags n),() #);
set hti = HT (I,T);
reconsider hti = HT (I,T) as Subset of RelStr(# (Bags n),() #) ;
consider S being finite Subset of (Bags n) such that
A15: S is_Dickson-basis_of hti, RelStr(# (Bags n),() #) by Th34;
set M = { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } where s is Element of Bags n : s in S } ;
set s = the Element of S;
reconsider q = q as Polynomial of n,L by POLYNOM1:def 11;
set hq = HT (q,T);
reconsider hq = HT (q,T) as Element of RelStr(# (Bags n),() #) ;
hq in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A14;
then ex b being Element of RelStr(# (Bags n),() #) st
( b in S & b <= hq ) by ;
then the Element of S in S ;
then { r where r is Polynomial of n,L : ( r in I & HT (r,T) = the Element of S & r <> 0_ (n,L) ) } in { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s9 & p <> 0_ (n,L) ) } where s9 is Element of Bags n : s9 in S } ;
then reconsider M = { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } where s is Element of Bags n : s in S } as non empty set ;
A16: for x, y being set st x in M & y in M & x <> y holds
x misses y
proof
let x, y be set ; :: thesis: ( x in M & y in M & x <> y implies x misses y )
assume that
A17: x in M and
A18: y in M and
A19: x <> y ; :: thesis: x misses y
consider t being Element of Bags n such that
A20: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = t & p <> 0_ (n,L) ) } and
t in S by A18;
consider s being Element of Bags n such that
A21: x = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and
s in S by A17;
reconsider x = x, y = y as set ;
now :: thesis: not x /\ y <> {}
set u = the Element of x /\ y;
assume A22: x /\ y <> {} ; :: thesis: contradiction
then the Element of x /\ y in y by XBOOLE_0:def 4;
then A23: ex v being Polynomial of n,L st
( the Element of x /\ y = v & v in I & HT (v,T) = t & v <> 0_ (n,L) ) by A20;
the Element of x /\ y in x by ;
then ex r being Polynomial of n,L st
( the Element of x /\ y = r & r in I & HT (r,T) = s & r <> 0_ (n,L) ) by A21;
hence contradiction by A19, A21, A20, A23; :: thesis: verum
end;
hence x misses y by XBOOLE_0:def 7; :: thesis: verum
end;
A24: S c= hti by ;
for x being set st x in M holds
x <> {}
proof
let x be set ; :: thesis: ( x in M implies x <> {} )
assume x in M ; :: thesis: x <> {}
then consider s being Element of Bags n such that
A25: x = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and
A26: s in S ;
s in hti by ;
then consider q being Polynomial of n,L such that
A27: ( s = HT (q,T) & q in I & q <> 0_ (n,L) ) ;
q in x by ;
hence x <> {} ; :: thesis: verum
end;
then consider G9 being set such that
A28: for x being set st x in M holds
ex y being object st G9 /\ x = {y} by ;
set xx = the Element of M;
A29: M is finite
proof
defpred S1[ object , object ] means \$2 = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = \$1 & p <> 0_ (n,L) ) } ;
A30: for x being object st x in S holds
ex y being object st S1[x,y] ;
consider f being Function such that
A31: ( dom f = S & ( for x being object st x in S holds
S1[x,f . x] ) ) from
A32: now :: thesis: for u being object st u in rng f holds
u in M
let u be object ; :: thesis: ( u in rng f implies u in M )
assume u in rng f ; :: thesis: u in M
then consider s being object such that
A33: s in dom f and
A34: u = f . s by FUNCT_1:def 3;
u = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } by ;
hence u in M by ; :: thesis: verum
end;
now :: thesis: for u being object st u in M holds
u in rng f
let u be object ; :: thesis: ( u in M implies u in rng f )
assume u in M ; :: thesis: u in rng f
then consider s being Element of Bags n such that
A35: u = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and
A36: s in S ;
f . s in rng f by ;
hence u in rng f by ; :: thesis: verum
end;
then rng f = M by ;
hence M is finite by ; :: thesis: verum
end;
A37: ex y being object st G9 /\ the Element of M = {y} by A28;
set xx = the Element of M;
reconsider G9 = G9 as non empty set by A37;
set G = { x where x is Element of G9 : ex y being set st
( y in M & G9 /\ y = {x} )
}
;
now :: thesis: for u being object st u in { x where x is Element of G9 : ex y being set st
( y in M & G9 /\ y = {x} )
}
holds
u in the carrier of (Polynom-Ring (n,L))
let u be object ; :: thesis: ( u in { x where x is Element of G9 : ex y being set st
( y in M & G9 /\ y = {x} )
}
implies u in the carrier of (Polynom-Ring (n,L)) )

assume u in { x where x is Element of G9 : ex y being set st
( y in M & G9 /\ y = {x} )
}
; :: thesis: u in the carrier of (Polynom-Ring (n,L))
then consider x being Element of G9 such that
A38: u = x and
A39: ex y being set st
( y in M & G9 /\ y = {x} ) ;
consider y being set such that
A40: y in M and
A41: G9 /\ y = {x} by A39;
consider s being Element of Bags n such that
A42: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and
s in S by A40;
x in G9 /\ y by ;
then x in y by XBOOLE_0:def 4;
then ex q being Polynomial of n,L st
( x = q & q in I & HT (q,T) = s & q <> 0_ (n,L) ) by A42;
hence u in the carrier of (Polynom-Ring (n,L)) by A38; :: thesis: verum
end;
then reconsider G = { x where x is Element of G9 : ex y being set st
( y in M & G9 /\ y = {x} )
}
as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;
defpred S1[ object , object ] means ex D1 being set st
( D1 = \$1 & G9 /\ D1 = {\$2} & \$2 in G );
A43: for x being object st x in M holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in M implies ex y being object st S1[x,y] )
assume A44: x in M ; :: thesis: ex y being object st S1[x,y]
reconsider xx = x as set by TARSKI:1;
consider y being object such that
A45: G9 /\ xx = {y} by ;
y in G9 /\ xx by ;
then reconsider y = y as Element of G9 by XBOOLE_0:def 4;
y in G by ;
hence ex y being object st S1[x,y] by A45; :: thesis: verum
end;
consider f being Function such that
A46: ( dom f = M & ( for x being object st x in M holds
S1[x,f . x] ) ) from
A47: now :: thesis: for u being object st u in G holds
u in rng f
let u be object ; :: thesis: ( u in G implies u in rng f )
assume u in G ; :: thesis: u in rng f
then consider x being Element of G9 such that
A48: u = x and
A49: ex y being set st
( y in M & G9 /\ y = {x} ) ;
consider y being set such that
A50: y in M and
A51: G9 /\ y = {x} by A49;
S1[y,f . y] by ;
then G9 /\ y = {(f . y)} ;
then A52: x in {(f . y)} by ;
f . y in rng f by ;
hence u in rng f by ; :: thesis: verum
end;
now :: thesis: for u being object st u in rng f holds
u in G
let u be object ; :: thesis: ( u in rng f implies u in G )
assume u in rng f ; :: thesis: u in G
then consider s being object such that
A53: ( s in dom f & u = f . s ) by FUNCT_1:def 3;
S1[s,f . s] by ;
hence u in G by A53; :: thesis: verum
end;
then A54: rng f = G by ;
consider y being object such that
A55: G9 /\ the Element of M = {y} by A28;
y in G9 /\ the Element of M by ;
then y in G9 by XBOOLE_0:def 4;
then y in G by A55;
then ( not G is empty & G is finite ) by ;
then reconsider G = G as non empty finite Subset of (Polynom-Ring (n,L)) ;
for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b )
proof
let b be bag of n; :: thesis: ( b in HT (I,T) implies ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b ) )

reconsider bb = b as Element of RelStr(# (Bags n),() #) by PRE_POLY:def 12;
assume b in HT (I,T) ; :: thesis: ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b )

then consider bb9 being Element of RelStr(# (Bags n),() #) such that
A56: bb9 in S and
A57: bb9 <= bb by ;
set N = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } ;
A58: { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } in M by A56;
then consider y being object such that
A59: G9 /\ { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } = {y} by A28;
reconsider b9 = bb9 as bag of n ;
take b9 ; :: thesis: ( b9 in HT (G,T) & b9 divides b )
A60: [bb9,bb] in DivOrder n by ;
A61: y in G9 /\ { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } by ;
then reconsider y = y as Element of G9 by XBOOLE_0:def 4;
y in { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } by ;
then A62: ex r being Polynomial of n,L st
( y = r & r in I & HT (r,T) = bb9 & r <> 0_ (n,L) ) ;
y in G by ;
hence ( b9 in HT (G,T) & b9 divides b ) by ; :: thesis: verum
end;
then A63: HT (I,T) c= multiples (HT (G,T)) by Th28;
take G ; :: thesis:
now :: thesis: for u being object st u in G holds
u in I
let u be object ; :: thesis: ( u in G implies u in I )
assume u in G ; :: thesis: u in I
then consider x being Element of G9 such that
A64: u = x and
A65: ex y being set st
( y in M & G9 /\ y = {x} ) ;
consider y being set such that
A66: y in M and
A67: G9 /\ y = {x} by A65;
consider s being Element of Bags n such that
A68: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and
s in S by A66;
x in G9 /\ y by ;
then x in y by XBOOLE_0:def 4;
then ex q being Polynomial of n,L st
( x = q & q in I & HT (q,T) = s & q <> 0_ (n,L) ) by A68;
hence u in I by A64; :: thesis: verum
end;
then G c= I ;
hence G is_Groebner_basis_of I,T by ; :: thesis: verum
end;
end;