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)) 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 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)) 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 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)) 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 :: 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 A4: u = 0_ (n,L) by TARSKI:def 1;

now :: thesis: u in I

assume not u in I ; :: thesis: contradiction
then for v being object 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 :: 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 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 11;
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:34;
reconsider hq = HT (q,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

A8: now :: thesis: S is finite

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:1; :: thesis: verum

end;

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

now :: thesis: for u being object st u in S holds
u in Bags n

let u be object ; :: 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 } ;
set s = the 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 the Element of S in S ;
then reconsider s = the Element of 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 :: thesis: for u being object st u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } holds
u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: 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 :: thesis: for q being Polynomial of n,L holds
( not q in I or not q < p9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) )

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 :: thesis: for q being Polynomial of n,L holds
( not q in I or not q < p9,T or not HM (q,T) = Monom ((1. L),s) )

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 :: thesis: for u being object st u in x holds
u in {p9}

let u be object ; :: 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 :: thesis: for q being Polynomial of n,L holds
( not q in I or not q < u9,T or not HM (q,T) = Monom ((1. L),s) )

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 object 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 :: thesis: for u being object st u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } holds
u in I

let u be object ; :: 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 ;
A46: M is finite

proof

defpred S₁[ object , object ] 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 object st x in S holds
ex y being object st S₁[x,y] ;
consider f being Function such that
A48: ( dom f = S & ( for x being object st x in S holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A47);

A49: 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
A50: s in dom f and
A51: u = f . s by FUNCT_1:def 3;
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 :: thesis: for v being object st 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) ) ) ) } holds
v in f . s

let v be object ; :: 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 :: thesis: for v being object st v in f . s holds
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) ) ) ) }

let v be object ; :: 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 :: 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 )
reconsider uu = u as set by TARSKI:1;
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 :: thesis: for v being object st v in uu holds
v in f . s

let v be object ; :: thesis: ( v in uu implies v in f . s )
assume v in uu ; :: 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 :: thesis: for v being object st v in f . s holds
v in uu

let v be object ; :: thesis: ( v in f . s implies v in uu )
assume v in f . s ; :: thesis: v in uu
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 uu by A54; :: thesis: verum

end;

f . s in rng f by A48, A55, FUNCT_1:3;
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:8; :: 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₁[ object , object ] 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 object st x in M holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in M implies ex y being object st S₁[x,y] )
assume A61: x in M ; :: thesis: ex y being object 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 object st x in M holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A60);

A64: now :: thesis: for u being object st u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } holds
u in rng f

let u be object ; :: 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:3;
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 :: thesis: for u being object st u in rng f holds
u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }

let u be object ; :: 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 object such that
A71: s in dom f and
A72: u = f . s by FUNCT_1:def 3;
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:8; :: thesis: verum

end;

now :: thesis: for u being object st u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } holds
u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: 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 11; :: 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

set z = the Element of M;
consider r being Polynomial of n,L such that
r in I and
A73: the Element of M = {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 5;
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 :: thesis: for q being Polynomial of n,L st q in G holds
( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )

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; :: 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 :: thesis: ( q is_reducible_wrt G \ {q},T implies q is_irreducible_wrt G \ {q},T )

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 :: thesis: ( ( b = HT (q,T) & q is_irreducible_wrt G \ {q},T ) or ( b <> HT (q,T) & contradiction ) )

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 :: thesis: not htg in {htq}

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

A112: now :: thesis: 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 \ {htq} & b <= a )

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 :: thesis: ( ( b in S \ {htq} & ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a ) ) or ( not b in S \ {htq} & ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S \ {htq} & b <= a ) ) )

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:3; :: 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 :: thesis: not htq in S \ {htq}

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

now :: thesis: not HT (q,T) < HT (pp,T),T

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 :: thesis: not pp = 0_ (n,L)

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 11;
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 11;
then q - (m *' g) = qq - (mm * gg) by Lm2;
then pp in I by A124, A125;
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 ; :: thesis: verum