let n be Element of NAT ; 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) 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; 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) 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 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) 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); 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 27;
per cases
( I = {(0_ n,L)} or I <> {(0_ n,L)} )
;
suppose A2:
I = {(0_ n,L)}
;
ex G being finite Subset of (Polynom-Ring n,L) st G is_Groebner_basis_of I,Tset G =
{(0_ n,L)};
set R =
PolyRedRel {(0_ n,L)},
T;
take
{(0_ n,L)}
;
{(0_ n,L)} is_Groebner_basis_of I,Tnow let a,
b,
c be
set ;
( [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
;
b,c are_convergent_wrt PolyRedRel {(0_ n,L)},Tconsider p,
q being
set 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 A3, ZFMISC_1:def 2;
reconsider q =
q as
Polynomial of
n,
L by A5, POLYNOM1:def 27;
not
p in {(0_ n,L)}
by A1, A4, XBOOLE_0:def 5;
then
p <> 0_ n,
L
by TARSKI:def 1;
then reconsider p =
p as
non-zero Polynomial of
n,
L by A4, POLYNOM1:def 27, POLYNOM7:def 2;
p reduces_to q,
{(0_ n,L)},
T
by A3, A6, POLYRED:def 13;
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 A7, TARSKI:def 1;
then
p is_reducible_wrt 0_ n,
L,
T
by A8, POLYRED:def 8;
hence
b,
c are_convergent_wrt PolyRedRel {(0_ n,L)},
T
by Lm3;
verum end; then A9:
PolyRedRel {(0_ n,L)},
T is
locally-confluent
by REWRITE1:def 24;
{(0_ n,L)} -Ideal = I
by A2, IDEAL_1:44;
hence
{(0_ n,L)} is_Groebner_basis_of I,
T
by A9, Def4;
verum end; suppose A10:
I <> {(0_ n,L)}
;
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
then consider q being
Element of
I such that A14:
q <> 0_ n,
L
;
set R =
RelStr(#
(Bags n),
(DivOrder n) #);
set hti =
HT I,
T;
reconsider hti =
HT I,
T as
Subset of
RelStr(#
(Bags n),
(DivOrder n) #) ;
consider S being
finite Subset of
(Bags n) such that A15:
S is_Dickson-basis_of hti,
RelStr(#
(Bags n),
(DivOrder 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 } ;
consider s being
Element of
S;
reconsider q =
q as
Polynomial of
n,
L by POLYNOM1:def 27;
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 A14;
then
ex
b being
Element of
RelStr(#
(Bags n),
(DivOrder n) #) st
(
b in S &
b <= hq )
by A15, DICKSON:def 9;
then
s in S
;
then
{ r where r is Polynomial of n,L : ( r in I & HT r,T = 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 ;
( 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
;
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;
now consider u being
Element of
x /\ y;
assume A22:
x /\ y <> {}
;
contradictionthen
u in y
by XBOOLE_0:def 4;
then A23:
ex
v being
Polynomial of
n,
L st
(
u = v &
v in I &
HT v,
T = t &
v <> 0_ n,
L )
by A20;
u in x
by A22, XBOOLE_0:def 4;
then
ex
r being
Polynomial of
n,
L st
(
u = r &
r in I &
HT r,
T = s &
r <> 0_ n,
L )
by A21;
hence
contradiction
by A19, A21, A20, A23;
verum end;
hence
x misses y
by XBOOLE_0:def 7;
verum
end; A24:
S c= hti
by A15, DICKSON:def 9;
for
x being
set st
x in M holds
x <> {}
then consider G9 being
set such that A28:
for
x being
set st
x in M holds
ex
y being
set st
G9 /\ x = {y}
by A16, WELLORD2:27;
consider xx being
Element of
M;
A29:
M is
finite
A37:
ex
y being
set st
G9 /\ xx = {y}
by A28;
consider xx being
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 let u be
set ;
( 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} ) }
;
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 A41, TARSKI:def 1;
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;
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[
set ,
set ]
means (
G9 /\ $1
= {$2} & $2
in G );
A43:
for
x being
set st
x in M holds
ex
y being
set st
S1[
x,
y]
consider f being
Function such that A46:
(
dom f = M & ( for
x being
set st
x in M holds
S1[
x,
f . x] ) )
from CLASSES1:sch 1(A43);
then A53:
rng f = G
by A47, TARSKI:2;
ex
y being
set st
G9 /\ xx = {y}
by A28;
then reconsider G =
G as non
empty finite Subset of
(Polynom-Ring n,L) by A29, A46, A53, FINSET_1:26;
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;
( 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
;
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 A54:
bb9 in S
and A55:
bb9 <= bb
by A15, DICKSON:def 9;
set N =
{ p where p is Polynomial of n,L : ( p in I & HT p,T = bb9 & p <> 0_ n,L ) } ;
A56:
{ p where p is Polynomial of n,L : ( p in I & HT p,T = bb9 & p <> 0_ n,L ) } in M
by A54;
then consider y being
set such that A57:
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
;
( b9 in HT G,T & b9 divides b )
A58:
[bb9,bb] in DivOrder n
by A55, ORDERS_2:def 9;
A59:
y in G9 /\ { p where p is Polynomial of n,L : ( p in I & HT p,T = bb9 & p <> 0_ n,L ) }
by A57, TARSKI:def 1;
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 A59, XBOOLE_0:def 4;
then A60:
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 A56, A57;
hence
(
b9 in HT G,
T &
b9 divides b )
by A58, A60, Def5;
verum
end; then A61:
HT I,
T c= multiples (HT G,T)
by Th28;
take
G
;
G is_Groebner_basis_of I,Tthen
G c= I
by TARSKI:def 3;
hence
G is_Groebner_basis_of I,
T
by A61, Th29;
verum