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

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;

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) #) ;
consider S being set such that
A6: ( S is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) & ( for C being set st C is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) holds
S c= C ) ) by DICKSON:35;
A7: ( S c= hti & ( for a being Element of RelStr(# (Bags n),(DivOrder n) #) st a in hti holds
ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S & b <= a ) ) ) by A6, DICKSON:def 9;

A8: now

assume A9: not S is finite ; :: thesis: contradiction
consider B being set such that
A10: ( B is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) & B is finite ) by DICKSON:def 10;
thus contradiction by A6, A9, A10, FINSET_1:13; :: thesis: verum

end;

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 A7;
then consider p being Polynomial of n,L such that
A11: ( u = HT p,T & p in I & p <> 0_ n,L ) ;
thus u in Bags n by A11; :: 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 } ;
set hq = HT q,T;
reconsider hq = HT q,T as Element of RelStr(# (Bags n),(DivOrder n) #) ;
hq in { (HT p,T) where p is Polynomial of n,L : ( p in I & p <> 0_ n,L ) } by A5;
then A12: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S & b <= hq ) by A6, DICKSON:def 9;
consider s being Element of S;
s in S by A12;
then reconsider s = s as Element of Bags n ;
set M' = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),(HT q,T) & p <> 0_ n,L ) } ;
{ 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 A12;
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 ;
A16: M is finite

proof

defpred S₁[ set , set ] means $2 = { p where p is Polynomial of n,L : ex b being bag of 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 ) ) ) } ;
A18: for x being set st x in S holds
ex y being set st S₁[x,y] ;
consider f being Function such that
A19: ( dom f = S & ( for x being set st x in S holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A18);

A20: 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
A21: ( 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 ) ) ) } & s in S ) ;
A22: f . s in rng f by A19, A21, FUNCT_1:12;
consider b being bag of such that
A23: f . s = { p where p is Polynomial of n,L : ex b being bag of 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 A19, A21;

A24: now

let v be set ; :: thesis: ( v in u implies v in f . s )
assume v in u ; :: thesis: v in f . s
then consider p being Polynomial of n,L such that
A25: ( 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 A21;
thus v in f . s by A23, A25; :: thesis: verum

end;

now

let v be set ; :: thesis: ( v in f . s implies v in u )
assume v in f . s ; :: thesis: v in u
then consider p being Polynomial of n,L such that
A26: ( v = p & ex b being bag of 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 A23;
thus v in u by A21, A26; :: thesis: verum

end;

hence u in rng f by A22, A24, TARSKI:2; :: thesis: verum

end;

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
A27: ( s in dom f & u = f . s ) by FUNCT_1:def 5;
reconsider s = s as Element of Bags n by A19, A27;
consider b being bag of such that
A28: f . s = { p where p is Polynomial of n,L : ex b being bag of 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 A19, A27;
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 ) ) ) } ;

A29: 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 consider p being Polynomial of n,L such that
A30: ( v = p & ex b being bag of 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 A28;
thus 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 ) ) ) } by A30; :: thesis: verum

end;

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 consider p being Polynomial of n,L such that
A31: ( 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 ) ) ) ;
thus v in f . s by A28, A31; :: 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 A27, A29, TARSKI:2;
hence u in M by A19, A27; :: thesis: verum

end;

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

end;

A32: 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
A33: ( 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 ) ) ) } & s in S ) ;
s in hti by A7, A33;
then consider q being Polynomial of n,L such that
A34: ( s = HT q,T & q in I & q <> 0_ n,L ) ;
consider qq being Polynomial of n,L such that
A35: ( qq in I & HM qq,T = Monom (1. L),(HT q,T) & qq <> 0_ n,L ) by A34, Lm10;
set M' = { p where p is Polynomial of n,L : ( p in I & HM p,T = Monom (1. L),s & p <> 0_ n,L ) } ;
A36: 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 A34, A35;

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 consider pp being Polynomial of n,L such that
A37: ( u = pp & pp in I & HM pp,T = Monom (1. L),s & pp <> 0_ n,L ) ;
thus u in the carrier of (Polynom-Ring n,L) by A37; :: thesis: verum

end;

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 ) } as non empty Subset of (Polynom-Ring n,L) by A36, TARSKI:def 3;
reconsider M' = M' as non empty Subset of (Polynom-Ring n,L) ;
consider p being Polynomial of n,L such that
A38: ( p in M' & ( for r being Polynomial of n,L st r in M' holds
p <= r,T ) ) by POLYRED:31;
consider p' being Polynomial of n,L such that
A39: ( p' = p & p' in I & HM p',T = Monom (1. L),s & p' <> 0_ n,L ) by A38;
take p' ; :: thesis: ( p' in I & x = {p'} & p' <> 0_ n,L )

A40: now

assume ex q being Polynomial of n,L st
( q in I & q < p',T & q <> 0_ n,L & HM q,T = Monom (1. L),s ) ; :: thesis: contradiction
then consider q being Polynomial of n,L such that
A41: ( q in I & q < p',T & q <> 0_ n,L & HM q,T = Monom (1. L),s ) ;
q in M' by A41;
then p <= q,T by A38;
hence contradiction by A39, A41, POLYRED:29; :: thesis: verum

end;

then A42: p' in x by A33, A39;

A43: now

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

end;

A46: for u being set st u in {p'} holds
u in x by A42, TARSKI:def 1;

now

let u be set ; :: thesis: ( u in x implies u in {p'} )
assume u in x ; :: thesis: u in {p'}
then consider u' being Polynomial of n,L such that
A47: ( u' = u & u' in I & HM u',T = Monom (1. L),s & 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),s ) ) ) by A33;

now

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

end;

then u' = p' by A39, A43, A47, Th37;
hence u in {p'} by A47, TARSKI:def 1; :: thesis: verum

end;

hence ( p' in I & x = {p'} & p' <> 0_ n,L ) by A39, A46, TARSKI:2; :: thesis: verum

end;

set G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ;

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
A50: ( u = r & ex x being Element of M st x = {r} ) ;
consider x being Element of M such that
A51: x = {r} by A50;
consider r' being Polynomial of n,L such that
A52: ( r' in I & x = {r'} & r' <> 0_ n,L ) by A32;
r' in {r} by A51, A52, TARSKI:def 1;
hence u in I by A50, A52, TARSKI:def 1; :: thesis: verum

end;

then A53: { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } c= I by TARSKI:def 3;
A54: { 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} );
A59: 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 A60: x in M ; :: thesis: ex y being set st S₁[x,y]
then reconsider x' = x as Element of M ;
consider q being Polynomial of n,L such that
A61: ( q in I & x = {q} & q <> 0_ n,L ) by A32, A60;
take q ; :: thesis: S₁[x,q]
take q ; :: thesis: ex x being Element of M st
( x = x & q = q & x = {q} )
take x' ; :: thesis: ( x = x' & q = q & x' = {q} )
thus x = x' ; :: thesis: ( q = q & x' = {q} )
thus q = q ; :: thesis: x' = {q}
thus x' = {q} by A61; :: thesis: verum

end;

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

A63: 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
A64: ( u = r & ex x being Element of M st x = {r} ) ;
consider x being Element of M such that
A65: x = {r} by A64;
A66: f . x in rng f by A62, FUNCT_1:12;
S₁[x,f . x] by A62;
then consider p' being Polynomial of n,L, x' being Element of M such that
A67: ( x' = x & p' = f . x & x = {p'} ) ;
p' in {r} by A65, A67, TARSKI:def 1;
hence u in rng f by A64, A66, A67, 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
A68: ( s in dom f & u = f . s ) by FUNCT_1:def 5;
reconsider s = s as Element of M by A62, A68;
consider p' being Polynomial of n,L, x' being Element of M such that
A69: ( x' = s & p' = f . s & x' = {p'} ) by A62;
thus u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } by A68, A69; :: thesis: verum

end;

then rng f = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } by A63, TARSKI:2;
hence { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is finite by A16, A62, 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 consider r being Polynomial of n,L such that
A70: ( u = r & ex x being Element of M st x = {r} ) ;
thus u in the carrier of (Polynom-Ring n,L) by A70, 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
A71: ( r in I & z = {r} & r <> 0_ n,L ) by A32;
r in G by A71;
hence G <> {} ; :: thesis: verum

end;

then reconsider G = G as non empty finite Subset of (Polynom-Ring n,L) by A54;
take G ; :: thesis: ( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
for b being bag of st b in HT I,T holds
ex b' being bag of st
( b' in HT G,T & b' divides b )

proof

let b be bag of ; :: thesis: ( b in HT I,T implies ex b' being bag of st
( b' in HT G,T & b' divides b ) )
assume A72: b in HT I,T ; :: thesis: ex b' being bag of st
( b' in HT G,T & b' divides b )
reconsider bb = b as Element of RelStr(# (Bags n),(DivOrder n) #) by POLYNOM1:def 14;
consider bb' being Element of RelStr(# (Bags n),(DivOrder n) #) such that
A73: ( bb' in S & bb' <= bb ) by A6, A72, DICKSON:def 9;
bb' is Element of Bags n ;
then reconsider b' = bb' as bag of ;
take b' ; :: thesis: ( b' in HT G,T & b' divides b )
A74: [bb',bb] in DivOrder n by A73, ORDERS_2:def 9;
set N = { p where p is Polynomial of n,L : ( 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' ) ) ) } ;
{ p where p is Polynomial of n,L : ( 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' ) ) ) } in M by A73;
then reconsider N = { p where p is Polynomial of n,L : ( 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' ) ) ) } as Element of M ;
consider r being Polynomial of n,L such that
A75: ( r in I & N = {r} & r <> 0_ n,L ) by A32;
r in N by A75, TARSKI:def 1;
then consider r' being Polynomial of n,L such that
A76: ( r = r' & r' in I & HM r',T = Monom (1. L),b' & r' <> 0_ n,L & ( for q being Polynomial of n,L holds
( not q in I or not q < r',T or not q <> 0_ n,L or not HM q,T = Monom (1. L),b' ) ) ) ;
1. L <> 0. L ;
then not 1. L is zero by STRUCT_0:def 15;
then A77: b' = term (HM r',T) by A76, POLYNOM7:10
.= HT r',T by TERMORD:22 ;
r' in G by A75, A76;
hence ( b' in HT G,T & b' divides b ) by A74, A76, A77, Def5; :: thesis: verum

end;

then HT I,T c= multiples (HT G,T) by Th28;
hence G is_Groebner_basis_of I,T by A53, 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 A78: 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
A79: ( q = rr & ex x being Element of M st x = {rr} ) ;
consider x being Element of M such that
A80: x = {rr} by A79;
x in M ;
then consider s being Element of Bags n such that
A81: ( 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 ) ) ) } & s in S ) ;
rr in x by A80, TARSKI:def 1;
then consider p being Polynomial of n,L such that
A82: ( rr = 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 A81;
A83: 1. L = coefficient (HM rr,T) by A82, POLYNOM7:9
.= HC rr,T by TERMORD:22 ;
hence q is_monic_wrt T by A79, Def6; :: thesis: q is_irreducible_wrt G \ {q},T
1. L <> 0. L ;
then not 1. L is zero by STRUCT_0:def 15;
then A84: s = term (HM rr,T) by A82, POLYNOM7:10
.= HT q,T by A79, TERMORD:22 ;

now

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
A85: q reduces_to pp,G \ {q},T by POLYRED:def 9;
consider g being Polynomial of n,L such that
A86: ( g in G \ {q} & q reduces_to pp,g,T ) by A85, POLYRED:def 7;
consider b being bag of such that
A87: q reduces_to pp,g,b,T by A86, POLYRED:def 6;
A88: ( q <> 0_ n,L & g <> 0_ n,L & b in Support q & ex s being bag of st
( s + (HT g,T) = b & pp = q - (((q . b) / (HC g,T)) * (s *' g)) ) ) by A87, POLYRED:def 5;
A89: ( g in G & not g in {q} ) by A86, XBOOLE_0:def 5;
reconsider htg = HT g,T as Element of RelStr(# (Bags n),(DivOrder n) #) ;
reconsider htq = HT q,T as Element of RelStr(# (Bags n),(DivOrder n) #) ;

now

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

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

then HT g,T divides HT q,T by A88, POLYNOM1:54;
then [htg,htq] in DivOrder n by Def5;
then A90: htg <= htq by ORDERS_2:def 9;
set S' = S \ {htq};
S \ {htq} c= S by XBOOLE_1:36;
then A91: S \ {htq} c= hti by A7, XBOOLE_1:1;
consider z being Polynomial of n,L such that
A92: ( g = z & ex x being Element of M st x = {z} ) by A89;
consider x1 being Element of M such that
A93: x1 = {z} by A92;
x1 in M ;
then consider t being Element of Bags n such that
A94: ( 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 ) ) ) } & t in S ) ;
z in x1 by A93, TARSKI:def 1;
then consider p1 being Polynomial of n,L such that
A95: ( z = p1 & p1 in I & HM p1,T = Monom (1. L),t & p1 <> 0_ n,L & ( 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 A94;
1. L <> 0. L ;
then not 1. L is zero by STRUCT_0:def 15;
then A96: t = term (HM p1,T) by A95, POLYNOM7:10
.= htg by A92, A95, TERMORD:22 ;

now

assume htg in {htq} ; :: thesis: contradiction
then t = s by A84, A96, TARSKI:def 1;
hence contradiction by A79, A80, A81, A89, A92, A93, A94, TARSKI:def 1; :: thesis: verum

end;

then A97: htg in S \ {htq} by A94, A96, XBOOLE_0:def 5;

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
A98: ( b in S & 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 A98; :: 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 A98, XBOOLE_0:def 5;
then htg <= b by A90, TARSKI:def 1;
hence ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a ) by A97, A98, 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;

then S \ {htq} is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) by A91, DICKSON:def 9;
then A99: S c= S \ {htq} by A6;

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;

hence q is_irreducible_wrt G \ {q},T by A81, A84, A99; :: thesis: verum

end;

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

A101: 1. L <> 0. L ;
b <= HT q,T,T by A88, TERMORD:def 6;
then b < HT q,T,T by A100, TERMORD:def 3;
then A102: pp . (HT q,T) = q . (HT q,T) by A87, POLYRED:41
.= 1. L by A79, A83, TERMORD:def 7 ;
then A103: HT q,T in Support pp by A101, POLYNOM1:def 9;
then A104: HT q,T <= HT pp,T,T by TERMORD:def 6;

now

assume A105: HT q,T < HT pp,T,T ; :: thesis: contradiction
then A106: ( HT q,T <= HT pp,T,T & b <= HT q,T,T ) by A88, TERMORD:def 3, TERMORD:def 6;
then A107: b <= HT pp,T,T by TERMORD:8;
b <> HT pp,T by A100, A106, TERMORD:7;
then b < HT pp,T,T by A107, TERMORD:def 3;
then ( HT pp,T in Support q iff HT pp,T in Support pp ) by A87, POLYRED:40;
then HT pp,T <= HT q,T,T by A103, TERMORD:def 6;
hence contradiction by A105, TERMORD:5; :: thesis: verum

end;

then HT pp,T <= HT q,T,T by TERMORD:5;
then HT pp,T = HT q,T by A104, TERMORD:7;
then Monom (HC pp,T),(HT pp,T) = Monom (1. L),s by A84, A102, TERMORD:def 7;
then A108: HM pp,T = HM q,T by A79, A82, TERMORD:def 8;
consider m being Monomial of n,L such that
A109: pp = q - (m *' g) by A86, 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 A86, XBOOLE_0:def 5;
then mm * gg in I by A53, IDEAL_1:def 2;
then - (mm * gg) in I by IDEAL_1:13;
then A110: qq + (- (mm * gg)) in I by A53, A78, IDEAL_1:def 1;
mm * gg = m *' g by POLYNOM1:def 27;
then q - (m *' g) = qq - (mm * gg) by Lm2;
then A111: pp in I by A109, A110, RLVECT_1:def 12;

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 A79, A83, A108, TERMORD:22 ;
hence contradiction ; :: thesis: verum

end;

hence contradiction by A79, A82, A86, A108, A111, 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