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 & not 0_ (n,L) in G )

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 & not 0_ (n,L) in G )

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 & not 0_ (n,L) in G )

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 & not 0_ (n,L) in G ) )

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 & not 0_ (n,L) in G )

A2: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

consider G being finite Subset of (Polynom-Ring (n,L)) such that

A3: G is_Groebner_basis_of I,T by Th35;

set R = PolyRedRel (G,T);

A4: G -Ideal = I by A3;

A5: PolyRedRel (G,T) is locally-confluent by A3;

set G9 = G \ {(0_ (n,L))};

set R9 = PolyRedRel ((G \ {(0_ (n,L))}),T);

reconsider G9 = G \ {(0_ (n,L))} as finite Subset of (Polynom-Ring (n,L)) ;

u in PolyRedRel ((G \ {(0_ (n,L))}),T)

then for u being object st u in PolyRedRel ((G \ {(0_ (n,L))}),T) holds

u in PolyRedRel (G,T) ;

then PolyRedRel ((G \ {(0_ (n,L))}),T) is locally-confluent by A5, A18, TARSKI:2;

then G9 is_Groebner_basis_of I,T by A6;

hence ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & not 0_ (n,L) in G ) by A17; :: thesis: verum

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 & not 0_ (n,L) in G )

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 & not 0_ (n,L) in G )

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 & not 0_ (n,L) in G )

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 & not 0_ (n,L) in G ) )

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 & not 0_ (n,L) in G )

A2: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

consider G being finite Subset of (Polynom-Ring (n,L)) such that

A3: G is_Groebner_basis_of I,T by Th35;

set R = PolyRedRel (G,T);

A4: G -Ideal = I by A3;

A5: PolyRedRel (G,T) is locally-confluent by A3;

set G9 = G \ {(0_ (n,L))};

set R9 = PolyRedRel ((G \ {(0_ (n,L))}),T);

reconsider G9 = G \ {(0_ (n,L))} as finite Subset of (Polynom-Ring (n,L)) ;

A6: now :: thesis: ( ( G9 = {} & G9 -Ideal = I ) or ( G9 <> {} & G9 -Ideal = I ) )end;

per cases
( G9 = {} or G9 <> {} )
;

end;

case A7:
G9 = {}
; :: thesis: G9 -Ideal = I

end;

now :: thesis: ( ( G = {} & G9 -Ideal = I ) or ( G <> {} & G9 -Ideal = I ) )end;

hence
G9 -Ideal = I
; :: thesis: verumper cases
( G = {} or G <> {} )
;

end;

case A8:
G <> {}
; :: thesis: G9 -Ideal = I

hence G9 -Ideal = I by A1, A4, A12, IDEAL_1:44; :: thesis: verum

end;

A9: now :: thesis: for u being object st u in {(0_ (n,L))} holds

u in G

A12:
0_ (n,L) = 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;u in G

let u be object ; :: thesis: ( u in {(0_ (n,L))} implies u in G )

assume u in {(0_ (n,L))} ; :: thesis: u in G

then A10: u = 0_ (n,L) by TARSKI:def 1;

A11: G c= {(0_ (n,L))} by A7, XBOOLE_1:37;

end;assume u in {(0_ (n,L))} ; :: thesis: u in G

then A10: u = 0_ (n,L) by TARSKI:def 1;

A11: G c= {(0_ (n,L))} by A7, XBOOLE_1:37;

now :: thesis: ( not u in G implies G = {} )

hence
u in G
by A8; :: thesis: verumassume
not u in G
; :: thesis: G = {}

then for v being object holds not v in G by A10, A11, TARSKI:def 1;

hence G = {} by XBOOLE_0:def 1; :: thesis: verum

end;then for v being object holds not v in G by A10, A11, TARSKI:def 1;

hence G = {} by XBOOLE_0:def 1; :: thesis: verum

now :: thesis: for u being object st u in G holds

u in {(0_ (n,L))}

then
G = {(0_ (n,L))}
by A9, TARSKI:2;u in {(0_ (n,L))}

let u be object ; :: thesis: ( u in G implies u in {(0_ (n,L))} )

assume A13: u in G ; :: thesis: u in {(0_ (n,L))}

G c= {(0_ (n,L))} by A7, XBOOLE_1:37;

hence u in {(0_ (n,L))} by A13; :: thesis: verum

end;assume A13: u in G ; :: thesis: u in {(0_ (n,L))}

G c= {(0_ (n,L))} by A7, XBOOLE_1:37;

hence u in {(0_ (n,L))} by A13; :: thesis: verum

hence G9 -Ideal = I by A1, A4, A12, IDEAL_1:44; :: thesis: verum

case
G9 <> {}
; :: thesis: G9 -Ideal = I

then reconsider GG = G, GG9 = G9 as non empty Subset of (Polynom-Ring (n,L)) ;

A14: 0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;

end;A14: 0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;

A15: now :: thesis: for u being object st u in G -Ideal holds

u in G9 -Ideal

u in G9 -Ideal

let u be object ; :: thesis: ( u in G -Ideal implies u in G9 -Ideal )

assume u in G -Ideal ; :: thesis: u in G9 -Ideal

then ex f being LinearCombination of GG st u = Sum f by IDEAL_1:60;

then ex g being LinearCombination of GG9 st u = Sum g by A14, Lm9;

hence u in G9 -Ideal by IDEAL_1:60; :: thesis: verum

end;assume u in G -Ideal ; :: thesis: u in G9 -Ideal

then ex f being LinearCombination of GG st u = Sum f by IDEAL_1:60;

then ex g being LinearCombination of GG9 st u = Sum g by A14, Lm9;

hence u in G9 -Ideal by IDEAL_1:60; :: thesis: verum

now :: thesis: for u being object st u in G9 -Ideal holds

u in G -Ideal

hence
G9 -Ideal = I
by A4, A15, TARSKI:2; :: thesis: verumu in G -Ideal

let u be object ; :: thesis: ( u in G9 -Ideal implies u in G -Ideal )

A16: GG9 -Ideal c= GG -Ideal by IDEAL_1:57, XBOOLE_1:36;

assume u in G9 -Ideal ; :: thesis: u in G -Ideal

hence u in G -Ideal by A16; :: thesis: verum

end;A16: GG9 -Ideal c= GG -Ideal by IDEAL_1:57, XBOOLE_1:36;

assume u in G9 -Ideal ; :: thesis: u in G -Ideal

hence u in G -Ideal by A16; :: thesis: verum

A17: now :: thesis: not 0_ (n,L) in G9

A18:
for u being object st u in PolyRedRel (G,T) holds assume
0_ (n,L) in G9
; :: thesis: contradiction

then not 0_ (n,L) in {(0_ (n,L))} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not 0_ (n,L) in {(0_ (n,L))} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

u in PolyRedRel ((G \ {(0_ (n,L))}),T)

proof

PolyRedRel ((G \ {(0_ (n,L))}),T) c= PolyRedRel (G,T)
by Th4, XBOOLE_1:36;
let u be object ; :: thesis: ( u in PolyRedRel (G,T) implies u in PolyRedRel ((G \ {(0_ (n,L))}),T) )

assume A19: u in PolyRedRel (G,T) ; :: thesis: u in PolyRedRel ((G \ {(0_ (n,L))}),T)

then consider p, q being object such that

A20: p in NonZero (Polynom-Ring (n,L)) and

A21: q in the carrier of (Polynom-Ring (n,L)) and

A22: u = [p,q] by ZFMISC_1:def 2;

reconsider q = q as Polynomial of n,L by A21, POLYNOM1:def 11;

not p in {(0_ (n,L))} by A2, A20, 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 A20, POLYNOM1:def 11, POLYNOM7:def 1;

p reduces_to q,G,T by A19, A22, POLYRED:def 13;

then consider f being Polynomial of n,L such that

A23: f in G and

A24: p reduces_to q,f,T by POLYRED:def 7;

ex b being bag of n st p reduces_to q,f,b,T by A24, POLYRED:def 6;

then f <> 0_ (n,L) by POLYRED:def 5;

then not f in {(0_ (n,L))} by TARSKI:def 1;

then f in G9 by A23, XBOOLE_0:def 5;

then p reduces_to q,G9,T by A24, POLYRED:def 7;

hence u in PolyRedRel ((G \ {(0_ (n,L))}),T) by A22, POLYRED:def 13; :: thesis: verum

end;assume A19: u in PolyRedRel (G,T) ; :: thesis: u in PolyRedRel ((G \ {(0_ (n,L))}),T)

then consider p, q being object such that

A20: p in NonZero (Polynom-Ring (n,L)) and

A21: q in the carrier of (Polynom-Ring (n,L)) and

A22: u = [p,q] by ZFMISC_1:def 2;

reconsider q = q as Polynomial of n,L by A21, POLYNOM1:def 11;

not p in {(0_ (n,L))} by A2, A20, 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 A20, POLYNOM1:def 11, POLYNOM7:def 1;

p reduces_to q,G,T by A19, A22, POLYRED:def 13;

then consider f being Polynomial of n,L such that

A23: f in G and

A24: p reduces_to q,f,T by POLYRED:def 7;

ex b being bag of n st p reduces_to q,f,b,T by A24, POLYRED:def 6;

then f <> 0_ (n,L) by POLYRED:def 5;

then not f in {(0_ (n,L))} by TARSKI:def 1;

then f in G9 by A23, XBOOLE_0:def 5;

then p reduces_to q,G9,T by A24, POLYRED:def 7;

hence u in PolyRedRel ((G \ {(0_ (n,L))}),T) by A22, POLYRED:def 13; :: thesis: verum

then for u being object st u in PolyRedRel ((G \ {(0_ (n,L))}),T) holds

u in PolyRedRel (G,T) ;

then PolyRedRel ((G \ {(0_ (n,L))}),T) is locally-confluent by A5, A18, TARSKI:2;

then G9 is_Groebner_basis_of I,T by A6;

hence ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & not 0_ (n,L) in G ) by A17; :: thesis: verum