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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st I <> {(0_ n,L)} holds
ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st I <> {(0_ n,L)} holds
ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st I <> {(0_ n,L)} holds
ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
let I be non empty add-closed left-ideal Subset of (Polynom-Ring n,L); :: thesis: ( I <> {(0_ n,L)} implies ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T ) )
set R = RelStr(# (Bags n),(DivOrder n) #);
assume A1: I <> {(0_ n,L)} ; :: thesis: ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
ex q being Element of I st q <> 0_ n,L

proof

assume A2: for q being Element of I holds not q <> 0_ n,L ; :: thesis: contradiction

A3: now

let u be set ; :: thesis: ( u in {(0_ n,L)} implies u in I )
assume u in {(0_ n,L)} ; :: thesis: u in I
then A4: u = 0_ n,L by TARSKI:def 1;

now

assume not u in I ; :: thesis: contradiction
then for v being set holds not v in I by A2, A4;
hence contradiction by XBOOLE_0:def 1; :: thesis: verum

end;

hence u in I ; :: thesis: verum

end;

now

let u be set ; :: 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 A2;
hence u in {(0_ n,L)} by TARSKI:def 1; :: thesis: verum

end;

hence contradiction by A1, A3, TARSKI:2; :: thesis: verum

end;

then consider q being Element of I such that
A5: q <> 0_ n,L ;
reconsider q = q as Polynomial of n,L by POLYNOM1:def 27;
HT q,T in { (HT p,T) where p is Polynomial of n,L : ( p in I & p <> 0_ n,L ) } by A5;
then reconsider hti = HT I,T as non empty Subset of RelStr(# (Bags n),(DivOrder n) #) ;
set hq = HT q,T;
consider S being set such that
A6: S is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) and
A7: for C being set st C is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) holds
S c= C by DICKSON:35;
reconsider hq = HT q,T as Element of RelStr(# (Bags n),(DivOrder n) #) ;

A8: now

A9: ex B being set st
( B is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) & B is finite ) by DICKSON:def 10;
assume not S is finite ; :: thesis: contradiction
hence contradiction by A7, A9, FINSET_1:13; :: thesis: verum

end;

A10: S c= hti by A6, DICKSON:def 9;

now

let u be set ; :: thesis: ( u in S implies u in Bags n )
assume u in S ; :: thesis: u in Bags n
then u in hti by A10;
hence u in Bags n ; :: thesis: verum

end;

then reconsider S = S as finite Subset of (Bags n) by A8, TARSKI:def 3;
set M = { { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } where s is Element of Bags n : s in S } ;
consider s being Element of S;
hq in { (HT p,T) where p is Polynomial of n,L : ( p in I & p <> 0_ n,L ) } by A5;
then A11: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S & b <= hq ) by A6, DICKSON:def 9;
then s in S ;
then reconsider s = s as Element of Bags n ;
{ p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for r being Polynomial of n,L holds
( not r in I or not r < p,T or not r <> 0_ n,L or not HM r,T = Monom (1. L),s ) ) ) } in { { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } where s is Element of Bags n : s in S } by A11;
then reconsider M = { { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } where s is Element of Bags n : s in S } as non empty set ;
set G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ;
A12: for x being set st x in M holds
ex q being Polynomial of n,L st
( q in I & x = {q} & q <> 0_ n,L )

proof

let x be set ; :: thesis: ( x in M implies ex q being Polynomial of n,L st
( q in I & x = {q} & q <> 0_ n,L ) )
assume x in M ; :: thesis: ex q being Polynomial of n,L st
( q in I & x = {q} & q <> 0_ n,L )
then consider s being Element of Bags n such that
A13: x = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } and
A14: s in S ;
s in hti by A10, A14;
then consider q being Polynomial of n,L such that
A15: s = HT q,T and
A16: ( q in I & q <> 0_ n,L ) ;
consider qq being Polynomial of n,L such that
A17: ( qq in I & HM qq,T = Monom (1. L),(HT q,T) & qq <> 0_ n,L ) by A16, Lm10;
set M9 = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L ) } ;

A18: now

let u be set ; :: thesis: ( u in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L ) } implies u in the carrier of (Polynom-Ring n,L) )
assume u in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L ) } ; :: thesis: u in the carrier of (Polynom-Ring n,L)
then ex pp being Polynomial of n,L st
( u = pp & pp in I & HM pp,T = Monom (1. L),s & pp <> 0_ n,L ) ;
hence u in the carrier of (Polynom-Ring n,L) ; :: thesis: verum

end;

qq in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L ) } by A15, A17;
then reconsider M9 = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L ) } as non empty Subset of (Polynom-Ring n,L) by A18, TARSKI:def 3;
reconsider M9 = M9 as non empty Subset of (Polynom-Ring n,L) ;
consider p being Polynomial of n,L such that
A19: p in M9 and
A20: for r being Polynomial of n,L st r in M9 holds
p <= r,T by POLYRED:31;
consider p9 being Polynomial of n,L such that
A21: p9 = p and
A22: p9 in I and
A23: HM p9,T = Monom (1. L),s and
A24: p9 <> 0_ n,L by A19;

A25: now

assume ex q being Polynomial of n,L st
( q in I & q < p9,T & q <> 0_ n,L & HM q,T = Monom (1. L),s ) ; :: thesis: contradiction
then consider q being Polynomial of n,L such that
A26: q in I and
A27: q < p9,T and
A28: ( q <> 0_ n,L & HM q,T = Monom (1. L),s ) ;
q in M9 by A26, A28;
then p <= q,T by A20;
hence contradiction by A21, A27, POLYRED:29; :: thesis: verum

end;

A29: now

A30: 1. L <> 0. L ;
assume ex q being Polynomial of n,L st
( q in I & q < p9,T & HM q,T = Monom (1. L),s ) ; :: thesis: contradiction
then consider q being Polynomial of n,L such that
A31: ( q in I & q < p9,T ) and
A32: HM q,T = Monom (1. L),s ;
HC q,T = coefficient (Monom (1. L),s) by A32, TERMORD:22
.= 1. L by POLYNOM7:9 ;
then q <> 0_ n,L by A30, TERMORD:17;
hence contradiction by A25, A31, A32; :: thesis: verum

end;

A33: now

let u be set ; :: thesis: ( u in x implies u in {p9} )
assume u in x ; :: thesis: u in {p9}
then consider u9 being Polynomial of n,L such that
A34: u9 = u and
A35: ( u9 in I & HM u9,T = Monom (1. L),s ) and
u9 <> 0_ n,L and
A36: for q being Polynomial of n,L holds
( not q in I or not q < u9,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) by A13;

now

A37: 1. L <> 0. L ;
assume ex q being Polynomial of n,L st
( q in I & q < u9,T & HM q,T = Monom (1. L),s ) ; :: thesis: contradiction
then consider q being Polynomial of n,L such that
A38: ( q in I & q < u9,T ) and
A39: HM q,T = Monom (1. L),s ;
HC q,T = coefficient (Monom (1. L),s) by A39, TERMORD:22
.= 1. L by POLYNOM7:9 ;
then q <> 0_ n,L by A37, TERMORD:17;
hence contradiction by A36, A38, A39; :: thesis: verum

end;

then u9 = p9 by A22, A23, A29, A35, Th37;
hence u in {p9} by A34, TARSKI:def 1; :: thesis: verum

end;

take p9 ; :: thesis: ( p9 in I & x = {p9} & p9 <> 0_ n,L )
p9 in x by A13, A22, A23, A24, A25;
then for u being set st u in {p9} holds
u in x by TARSKI:def 1;
hence ( p9 in I & x = {p9} & p9 <> 0_ n,L ) by A22, A24, A33, TARSKI:2; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } implies u in I )
assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in I
then consider r being Polynomial of n,L such that
A40: u = r and
A41: ex x being Element of M st x = {r} ;
consider x being Element of M such that
A42: x = {r} by A41;
consider r9 being Polynomial of n,L such that
A43: r9 in I and
A44: x = {r9} and
r9 <> 0_ n,L by A12;
r9 in {r} by A42, A44, TARSKI:def 1;
hence u in I by A40, A43, TARSKI:def 1; :: thesis: verum

end;

then A45: { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } c= I by TARSKI:def 3;
A46: M is finite

proof

defpred S₁[ set , set ] means $2 = { p where p is Polynomial of n,L : ex b being bag of n st
( b = $1 & p in I & HM p,T = Monom (1. L),b & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b ) ) ) } ;
A47: for x being set st x in S holds
ex y being set st S₁[x,y] ;
consider f being Function such that
A48: ( dom f = S & ( for x being set st x in S holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A47);

A49: now

let u be set ; :: thesis: ( u in rng f implies u in M )
assume u in rng f ; :: thesis: u in M
then consider s being set such that
A50: s in dom f and
A51: u = f . s by FUNCT_1:def 5;
reconsider s = s as Element of Bags n by A48, A50;
set V = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } ;
A52: ex b being bag of n st f . s = { p where p is Polynomial of n,L : ex b being bag of n st
( b = s & p in I & HM p,T = Monom (1. L),b & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b ) ) ) } by A48, A50;

A53: now

let v be set ; :: thesis: ( v in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } implies v in f . s )
assume v in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } ; :: thesis: v in f . s
then ex p being Polynomial of n,L st
( v = p & p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) ;
hence v in f . s by A52; :: thesis: verum

end;

now

let v be set ; :: thesis: ( v in f . s implies v in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } )
assume v in f . s ; :: thesis: v in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) }
then ex p being Polynomial of n,L st
( v = p & ex b being bag of n st
( b = s & p in I & HM p,T = Monom (1. L),b & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b ) ) ) ) by A52;
hence v in { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } ; :: thesis: verum

end;

then u = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } by A51, A53, TARSKI:2;
hence u in M by A48, A50; :: thesis: verum

end;

now

let u be set ; :: 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
A54: u = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } and
A55: s in S ;
A56: ex b being bag of n st f . s = { p where p is Polynomial of n,L : ex b being bag of n st
( b = s & p in I & HM p,T = Monom (1. L),b & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b ) ) ) } by A48, A55;

A57: now

let v be set ; :: thesis: ( v in u implies v in f . s )
assume v in u ; :: thesis: v in f . s
then ex p being Polynomial of n,L st
( v = p & p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) by A54;
hence v in f . s by A56; :: thesis: verum

end;

A58: now

let v be set ; :: thesis: ( v in f . s implies v in u )
assume v in f . s ; :: thesis: v in u
then ex p being Polynomial of n,L st
( v = p & ex b being bag of n st
( b = s & p in I & HM p,T = Monom (1. L),b & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b ) ) ) ) by A56;
hence v in u by A54; :: thesis: verum

end;

f . s in rng f by A48, A55, FUNCT_1:12;
hence u in rng f by A57, A58, TARSKI:2; :: thesis: verum

end;

then rng f = M by A49, TARSKI:2;
hence M is finite by A48, FINSET_1:26; :: thesis: verum

end;

A59: { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is finite

proof

defpred S₁[ set , set ] means ex p being Polynomial of n,L ex x being Element of M st
( $1 = x & $2 = p & x = {p} );
A60: for x being set st x in M holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in M implies ex y being set st S₁[x,y] )
assume A61: x in M ; :: thesis: ex y being set st S₁[x,y]
then reconsider x9 = x as Element of M ;
consider q being Polynomial of n,L such that
q in I and
A62: x = {q} and
q <> 0_ n,L by A12, A61;
take q ; :: thesis: S₁[x,q]
take q ; :: thesis: ex x being Element of M st
( x = x & q = q & x = {q} )
take x9 ; :: thesis: ( x = x9 & q = q & x9 = {q} )
thus x = x9 ; :: thesis: ( q = q & x9 = {q} )
thus q = q ; :: thesis: x9 = {q}
thus x9 = {q} by A62; :: thesis: verum

end;

consider f being Function such that
A63: ( dom f = M & ( for x being set st x in M holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A60);

A64: now

let u be set ; :: thesis: ( u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } implies u in rng f )
assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in rng f
then consider r being Polynomial of n,L such that
A65: u = r and
A66: ex x being Element of M st x = {r} ;
consider x being Element of M such that
A67: x = {r} by A66;
S₁[x,f . x] by A63;
then consider p9 being Polynomial of n,L, x9 being Element of M such that
x9 = x and
A68: p9 = f . x and
A69: x = {p9} ;
A70: f . x in rng f by A63, FUNCT_1:12;
p9 in {r} by A67, A69, TARSKI:def 1;
hence u in rng f by A65, A70, A68, TARSKI:def 1; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in rng f implies u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } )
assume u in rng f ; :: thesis: u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }
then consider s being set such that
A71: s in dom f and
A72: u = f . s by FUNCT_1:def 5;
reconsider s = s as Element of M by A63, A71;
ex p9 being Polynomial of n,L ex x9 being Element of M st
( x9 = s & p9 = f . s & x9 = {p9} ) by A63;
hence u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } by A72; :: thesis: verum

end;

then rng f = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } by A64, TARSKI:2;
hence { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is finite by A46, A63, FINSET_1:26; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } implies u in the carrier of (Polynom-Ring n,L) )
assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in the carrier of (Polynom-Ring n,L)
then ex r being Polynomial of n,L st
( u = r & ex x being Element of M st x = {r} ) ;
hence u in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27; :: thesis: verum

end;

then reconsider G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } as Subset of (Polynom-Ring n,L) by TARSKI:def 3;
G <> {}

proof

consider z being Element of M;
consider r being Polynomial of n,L such that
r in I and
A73: z = {r} and
r <> 0_ n,L by A12;
r in G by A73;
hence G <> {} ; :: thesis: verum

end;

then reconsider G = G as non empty finite Subset of (Polynom-Ring n,L) by A59;
take G ; :: thesis: ( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
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),(DivOrder 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),(DivOrder n) #) such that
A74: bb9 in S and
A75: bb9 <= bb by A6, DICKSON:def 9;
A76: [bb9,bb] in DivOrder n by A75, ORDERS_2:def 9;
reconsider b9 = bb9 as bag of n ;
set N = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),b9 & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b9 ) ) ) } ;
{ p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),b9 & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b9 ) ) ) } in M by A74;
then reconsider N = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),b9 & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b9 ) ) ) } as Element of M ;
take b9 ; :: thesis: ( b9 in HT G,T & b9 divides b )
consider r being Polynomial of n,L such that
r in I and
A77: N = {r} and
r <> 0_ n,L by A12;
r in N by A77, TARSKI:def 1;
then consider r9 being Polynomial of n,L such that
A78: r = r9 and
r9 in I and
A79: HM r9,T = Monom (1. L),b9 and
A80: r9 <> 0_ n,L and
for q being Polynomial of n,L holds
( not q in I or not q < r9,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b9 ) ;
A81: r9 in G by A77, A78;
b9 = term (HM r9,T) by A79, POLYNOM7:10
.= HT r9,T by TERMORD:22 ;
hence ( b9 in HT G,T & b9 divides b ) by A76, A80, A81, Def5; :: thesis: verum

end;

then HT I,T c= multiples (HT G,T) by Th28;
hence G is_Groebner_basis_of I,T by A45, Th29; :: thesis: G is_reduced_wrt T

now

let q be Polynomial of n,L; :: thesis: ( q in G implies ( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T ) )
assume A82: q in G ; :: thesis: ( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )
then consider rr being Polynomial of n,L such that
A83: q = rr and
A84: ex x being Element of M st x = {rr} ;
consider x being Element of M such that
A85: x = {rr} by A84;
x in M ;
then consider s being Element of Bags n such that
A86: x = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) ) ) } and
A87: s in S ;
rr in x by A85, TARSKI:def 1;
then consider p being Polynomial of n,L such that
A88: rr = p and
p in I and
A89: HM p,T = Monom (1. L),s and
p <> 0_ n,L and
A90: for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),s ) by A86;
A91: 1. L = coefficient (HM rr,T) by A88, A89, POLYNOM7:9
.= HC rr,T by TERMORD:22 ;
hence q is_monic_wrt T by A83, Def6; :: thesis: q is_irreducible_wrt G \ {q},T
A92: s = term (HM rr,T) by A88, A89, POLYNOM7:10
.= HT q,T by A83, TERMORD:22 ;

now

reconsider htq = HT q,T as Element of RelStr(# (Bags n),(DivOrder n) #) ;
assume q is_reducible_wrt G \ {q},T ; :: thesis: q is_irreducible_wrt G \ {q},T
then consider pp being Polynomial of n,L such that
A93: q reduces_to pp,G \ {q},T by POLYRED:def 9;
consider g being Polynomial of n,L such that
A94: g in G \ {q} and
A95: q reduces_to pp,g,T by A93, POLYRED:def 7;
A96: g in G by A94, XBOOLE_0:def 5;
A97: not g in {q} by A94, XBOOLE_0:def 5;
reconsider htg = HT g,T as Element of RelStr(# (Bags n),(DivOrder n) #) ;
consider b being bag of n such that
A98: q reduces_to pp,g,b,T by A95, POLYRED:def 6;
A99: b in Support q by A98, POLYRED:def 5;
A100: ex s being bag of n st
( s + (HT g,T) = b & pp = q - (((q . b) / (HC g,T)) * (s *' g)) ) by A98, POLYRED:def 5;

now

per cases ( b = HT q,T or b <> HT q,T ) ;

case A101: b = HT q,T ; :: thesis: q is_irreducible_wrt G \ {q},T

set S9 = S \ {htq};
consider z being Polynomial of n,L such that
A102: g = z and
A103: ex x being Element of M st x = {z} by A96;
consider x1 being Element of M such that
A104: x1 = {z} by A103;
x1 in M ;
then consider t being Element of Bags n such that
A105: x1 = { u where u is Polynomial of n,L : ( u in I & HM u,T = Monom (1. L),t & u <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < u,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),t ) ) ) } and
A106: t in S ;
z in x1 by A104, TARSKI:def 1;
then consider p1 being Polynomial of n,L such that
A107: z = p1 and
p1 in I and
A108: HM p1,T = Monom (1. L),t and
p1 <> 0_ n,L and
for q being Polynomial of n,L holds
( not q in I or not q < p1,T or not q <> 0_ n,L or not HM q,T = Monom (1. L),t ) by A105;
A109: t = term (HM p1,T) by A108, POLYNOM7:10
.= htg by A102, A107, TERMORD:22 ;

now

assume htg in {htq} ; :: thesis: contradiction
then t = s by A92, A109, TARSKI:def 1;
hence contradiction by A83, A85, A86, A97, A102, A104, A105, TARSKI:def 1; :: thesis: verum

end;

then A110: htg in S \ {htq} by A106, A109, XBOOLE_0:def 5;
HT g,T divides HT q,T by A100, A101, PRE_POLY:50;
then [htg,htq] in DivOrder n by Def5;
then A111: htg <= htq by ORDERS_2:def 9;

A112: now

let a be Element of RelStr(# (Bags n),(DivOrder n) #); :: thesis: ( a in hti implies ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a ) )
assume a in hti ; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a )
then consider b being Element of RelStr(# (Bags n),(DivOrder n) #) such that
A113: b in S and
A114: b <= a by A6, DICKSON:def 9;

now

per cases ( b in S \ {htq} or not b in S \ {htq} ) ;

case b in S \ {htq} ; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a )

hence ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a ) by A114; :: thesis: verum

end;

case not b in S \ {htq} ; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a )

then b in {htq} by A113, XBOOLE_0:def 5;
then htg <= b by A111, TARSKI:def 1;
hence ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a ) by A110, A114, ORDERS_2:26; :: thesis: verum

end;

end;

end;

hence ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a ) ; :: thesis: verum

end;

A115: now

assume htq in S \ {htq} ; :: thesis: contradiction
then not htq in {htq} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

S \ {htq} c= S by XBOOLE_1:36;
then S \ {htq} c= hti by A10, XBOOLE_1:1;
then S \ {htq} is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) by A112, DICKSON:def 9;
then S c= S \ {htq} by A7;
hence q is_irreducible_wrt G \ {q},T by A87, A92, A115; :: thesis: verum

end;

case A116: b <> HT q,T ; :: thesis: contradiction

b <= HT q,T,T by A99, TERMORD:def 6;
then b < HT q,T,T by A116, TERMORD:def 3;
then A117: pp . (HT q,T) = q . (HT q,T) by A98, POLYRED:41
.= 1. L by A83, A91, TERMORD:def 7 ;
1. L <> 0. L ;
then A118: HT q,T in Support pp by A117, POLYNOM1:def 9;

now

A119: b <= HT q,T,T by A99, TERMORD:def 6;
assume A120: HT q,T < HT pp,T,T ; :: thesis: contradiction
then HT q,T <= HT pp,T,T by TERMORD:def 3;
then ( b <= HT pp,T,T & b <> HT pp,T ) by A116, A119, TERMORD:7, TERMORD:8;
then b < HT pp,T,T by TERMORD:def 3;
then ( HT pp,T in Support q iff HT pp,T in Support pp ) by A98, POLYRED:40;
then HT pp,T <= HT q,T,T by A118, TERMORD:def 6;
hence contradiction by A120, TERMORD:5; :: thesis: verum

end;

then A121: HT pp,T <= HT q,T,T by TERMORD:5;
HT q,T <= HT pp,T,T by A118, TERMORD:def 6;
then HT pp,T = HT q,T by A121, TERMORD:7;
then Monom (HC pp,T),(HT pp,T) = Monom (1. L),s by A92, A117, TERMORD:def 7;
then A122: HM pp,T = HM q,T by A83, A88, A89, TERMORD:def 8;

A123: now

assume pp = 0_ n,L ; :: thesis: contradiction
then 0. L = HC pp,T by TERMORD:17
.= coefficient (HM pp,T) by TERMORD:22
.= 1. L by A83, A91, A122, TERMORD:22 ;
hence contradiction ; :: thesis: verum

end;

consider m being Monomial of n,L such that
A124: pp = q - (m *' g) by A95, Th1;
reconsider gg = g, qq = q, mm = m as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider gg = gg, qq = qq, mm = mm as Element of (Polynom-Ring n,L) ;
g in G by A94, XBOOLE_0:def 5;
then mm * gg in I by A45, IDEAL_1:def 2;
then - (mm * gg) in I by IDEAL_1:13;
then A125: qq + (- (mm * gg)) in I by A45, A82, IDEAL_1:def 1;
mm * gg = m *' g by POLYNOM1:def 27;
then q - (m *' g) = qq - (mm * gg) by Lm2;
then pp in I by A124, A125, RLVECT_1:def 14;
hence contradiction by A83, A88, A89, A90, A95, A122, A123, POLYRED:43; :: thesis: verum

end;

end;

end;

hence q is_irreducible_wrt G \ {q},T ; :: thesis: verum

end;

hence q is_irreducible_wrt G \ {q},T ; :: thesis: verum

end;

hence G is_reduced_wrt T by Def7; :: thesis: verum
set M9 = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),(HT q,T) & p <> 0_ n,L ) } ;