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

for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,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))

for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,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))

for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let G be Subset of (Polynom-Ring (n,L)); :: thesis: for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let p be Polynomial of n,L; :: thesis: for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let q be non-zero Polynomial of n,L; :: thesis: ( p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T implies G \ {p} is_Groebner_basis_of I,T )

assume that

A1: p in G and

A2: q in G and

A3: p <> q and

A4: HT (q,T) divides HT (p,T) ; :: thesis: ( not G is_Groebner_basis_of I,T or G \ {p} is_Groebner_basis_of I,T )

reconsider GG = G as non empty Subset of (Polynom-Ring (n,L)) by A1;

assume A5: G is_Groebner_basis_of I,T ; :: thesis: G \ {p} is_Groebner_basis_of I,T

set G9 = G \ {p};

A6: not q in {p} by A3, TARSKI:def 1;

then ( q <> 0_ (n,L) & q in G \ {p} ) by A2, POLYNOM7:def 1, XBOOLE_0:def 5;

then A7: HT (q,T) in { (HT (u,T)) where u is Polynomial of n,L : ( u in G \ {p} & u <> 0_ (n,L) ) } ;

GG c= GG -Ideal by IDEAL_1:def 14;

then A8: G c= I by A5;

for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) by A1, A5, Th24;

then for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T by Th25;

then A9: for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T by A8, Th26;

for b being bag of n st b in HT (I,T) holds

ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b )

G \ {p} c= G by XBOOLE_1:36;

then A16: G \ {p} c= I by A8;

G \ {p} <> {} by A2, A6, XBOOLE_0:def 5;

hence G \ {p} is_Groebner_basis_of I,T by A16, A15, Th29; :: 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))

for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,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))

for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,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))

for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G being Subset of (Polynom-Ring (n,L))

for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let G be Subset of (Polynom-Ring (n,L)); :: thesis: for p being Polynomial of n,L

for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let p be Polynomial of n,L; :: thesis: for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds

G \ {p} is_Groebner_basis_of I,T

let q be non-zero Polynomial of n,L; :: thesis: ( p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T implies G \ {p} is_Groebner_basis_of I,T )

assume that

A1: p in G and

A2: q in G and

A3: p <> q and

A4: HT (q,T) divides HT (p,T) ; :: thesis: ( not G is_Groebner_basis_of I,T or G \ {p} is_Groebner_basis_of I,T )

reconsider GG = G as non empty Subset of (Polynom-Ring (n,L)) by A1;

assume A5: G is_Groebner_basis_of I,T ; :: thesis: G \ {p} is_Groebner_basis_of I,T

set G9 = G \ {p};

A6: not q in {p} by A3, TARSKI:def 1;

then ( q <> 0_ (n,L) & q in G \ {p} ) by A2, POLYNOM7:def 1, XBOOLE_0:def 5;

then A7: HT (q,T) in { (HT (u,T)) where u is Polynomial of n,L : ( u in G \ {p} & u <> 0_ (n,L) ) } ;

GG c= GG -Ideal by IDEAL_1:def 14;

then A8: G c= I by A5;

for f being Polynomial of n,L st f in I holds

PolyRedRel (G,T) reduces f, 0_ (n,L) by A1, A5, Th24;

then for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T by Th25;

then A9: for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T by A8, Th26;

for b being bag of n st b in HT (I,T) holds

ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b )

proof

then A15:
HT (I,T) c= multiples (HT ((G \ {p}),T))
by Th28;
let b be bag of n; :: thesis: ( b in HT (I,T) implies ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b ) )

assume b in HT (I,T) ; :: thesis: ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b )

then consider bb being bag of n such that

A10: bb in HT (G,T) and

A11: bb divides b by A9, Th27;

consider r being Polynomial of n,L such that

A12: bb = HT (r,T) and

A13: r in G and

A14: r <> 0_ (n,L) by A10;

( b9 in HT ((G \ {p}),T) & b9 divides b ) ; :: thesis: verum

end;( b9 in HT ((G \ {p}),T) & b9 divides b ) )

assume b in HT (I,T) ; :: thesis: ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b )

then consider bb being bag of n such that

A10: bb in HT (G,T) and

A11: bb divides b by A9, Th27;

consider r being Polynomial of n,L such that

A12: bb = HT (r,T) and

A13: r in G and

A14: r <> 0_ (n,L) by A10;

now :: thesis: ( ( r = p & ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b ) ) or ( r <> p & ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b ) ) )end;

hence
ex b9 being bag of n st ( b9 in HT ((G \ {p}),T) & b9 divides b ) ) or ( r <> p & ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b ) ) )

per cases
( r = p or r <> p )
;

end;

case
r = p
; :: thesis: ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b )

( b9 in HT ((G \ {p}),T) & b9 divides b )

hence
ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b ) by A4, A7, A11, A12, Lm8; :: thesis: verum

end;( b9 in HT ((G \ {p}),T) & b9 divides b ) by A4, A7, A11, A12, Lm8; :: thesis: verum

case
r <> p
; :: thesis: ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b )

( b9 in HT ((G \ {p}),T) & b9 divides b )

then
not r in {p}
by TARSKI:def 1;

then r in G \ {p} by A13, XBOOLE_0:def 5;

then bb in { (HT (u,T)) where u is Polynomial of n,L : ( u in G \ {p} & u <> 0_ (n,L) ) } by A12, A14;

hence ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b ) by A11; :: thesis: verum

end;then r in G \ {p} by A13, XBOOLE_0:def 5;

then bb in { (HT (u,T)) where u is Polynomial of n,L : ( u in G \ {p} & u <> 0_ (n,L) ) } by A12, A14;

hence ex b9 being bag of n st

( b9 in HT ((G \ {p}),T) & b9 divides b ) by A11; :: thesis: verum

( b9 in HT ((G \ {p}),T) & b9 divides b ) ; :: thesis: verum

G \ {p} c= G by XBOOLE_1:36;

then A16: G \ {p} c= I by A8;

G \ {p} <> {} by A2, A6, XBOOLE_0:def 5;

hence G \ {p} is_Groebner_basis_of I,T by A16, A15, Th29; :: thesis: verum